Theorem 19.20i 989

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 981	. 2 |- (A.xph -> ps)
3	2	a5i 986	1 |- (A.xph -> A.xps)

Syntax hints:   -> wi 3  A.wal 951

This theorem is referenced by:  19.20i2 990  19.20 991  19.20ii 992  19.21ai 995  hbal 1002  ax67 1016  ax67to6 1017  ax67to7 1018  ax467 1019  ax467to6 1021  ax467to7 1022  19.9d 1033  19.18 1046  19.26 1063  19.25 1080  19.33 1087  19.33b 1088  hbimd 1106  19.21t 1111  equid 1122  ax10 1137  a4im 1155  stdpc4 1181  sbied 1191  aev 1204  ax11 1214  hbsb4 1243  sbco3 1252  sbcom 1253  sb9i 1258  ax16i 1265  sbal1 1341  sbal2 1351  ax11eq 1356  ax11el 1357  ax11indi 1360  a12stdy3 1367  a12study 1371  mo 1386  eumo0 1388  mo2 1393  2mo 1440  bm1.1 1455  alral 1684  rgen2a 1691  r19.20i2 1695  r19.27av 1746  ceqsalg 1816  elabgt 1886  reu3 1921  sbciegft 1949  csbexg 1998  csbiegft 2019  csbnestg 2026  sbcnestg 2028  rabss2 2119  unss1 2189  ssrin 2224  undif4 2315  ralf0 2349  intmin4 2549  iinss 2590  axrep1 2684  axrep2 2685  bm1.3ii 2696  axnul 2699  axpr 2768  ssrel 3237  asymref2 3424  asymref2OLD 3426  funin 3552  zfrep6 3600  fv3 3718  tfrlem5 3900  dfom3 4602  aceq5 4712  aceq6a 4713  aceq6b 4714  kmlem1 4737  kmlem13 4749  zorn 4769  brdom3 4773  brdom4 4775  axpowndlem2 4922  axacndlem1 4931  axacndlem2 4932  axacndlem3 4933  axacndlem4 4934  axacnd 4936  suppsr2 5195  suppsr3 5196  pre-axsup 5263  peano2nn 5883  islp2 7688  chsscm 9033  chcmh 9034  pjnormss 10007

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

Copyright terms: Public domain