Theorem 19.20i 691

Description: Inference quantifying both antecedent and consequent.

Hypothesis

Ref	Expression
19.20i.1	|- (ph -> ps)

Assertion

Ref	Expression
19.20i	|- (A.xph -> A.xps)

Proof of Theorem 19.20i

Step	Hyp	Ref	Expression
1		19.20i.1	. . 3 |- (ph -> ps)
2	1	a4s 682	. 2 |- (A.xph -> ps)
3	2	a5i 687	1 |- (A.xph -> A.xps)

Syntax hints:   -> wi 2  A.wal 672

This theorem is referenced by:  19.20ii 692  hbne 699  hbal 700  hbim 702  19.9r 718  19.9d 720  19.12 729  19.18 732  19.21 738  19.21ai 740  19.26 749  19.25 763  19.33 770  19.33b 771  hbimd 787  19.21g 792  eqid 810  eq4 821  a4a 842  stdpc4 869  sb6y 872  sbied 903  hbsb4 905  ddelimdf 909  sbco3 915  sbcom 916  sb9i 920  sbal1 996  sbal2 1005  mo 1020  eumo0 1022  mo2 1026  bm1.1 1088  rgen2 1248  r19.20i2 1252  r19.27av 1293  ceqsalg 1362  axrep 1473  bm1.3ii 1481  unss1 1627  ssrin 1661  undif4 1744  zfnul 1746  iinss 2025  tfi 2244  relss 2480  funin 2708  zfrep6 2744  fv3 2839  tfrlem5 2953  tz7.48lem 2993  dfom3 3477  aceq5 3563  aceq6a 3564  aceq6b 3565  kmlem1 3580  kmlem12 3591  zorn2 3612  axpowndlem2 3744  axacndlem1 3753  axacndlem2 3754  axacndlem3 3755  axacndlem4 3756  axacnd 3758  suppsr2 4017  suppsr3 4018  axsup 4088  peano2nn 4433  chsscm 5147  chcmh 5148  pjnormss 5638

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

metamath.org