Theorem 19.20i 1033

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

Syntax hints:   -> wi 3  A.wal 995

This theorem is referenced by:  19.20i2 1034  19.20 1035  19.20ii 1036  19.21ai 1039  hbal 1046  ax67 1061  ax67to6 1062  ax67to7 1063  ax467 1064  ax467to6 1066  ax467to7 1067  19.9d 1078  19.18 1091  19.26 1108  19.25 1125  19.33 1132  19.33b 1133  hbimd 1151  19.21t 1156  equid 1167  ax10 1183  a4im 1201  stdpc4 1227  sbied 1237  aev 1250  ax11 1261  hbsb4 1290  sbco3 1299  sbcom 1300  sb9i 1305  ax16i 1312  sbal1 1388  sbal2 1400  ax11eq 1405  ax11el 1406  ax11indi 1409  a12stdy3 1416  a12study 1420  mo 1435  eumo0 1437  mo2 1442  2mo 1490  euequ1OLD 1501  bm1.1 1508  alral 1739  rgen2a 1746  r19.20i2 1750  r19.27av 1801  ceqsalg 1872  elabgt 1942  reu3 1978  sbciegft 2009  csbexg 2059  csbiegft 2080  csbnestg 2087  sbcnestg 2089  rabss2 2180  unss1 2250  ssrin 2285  undif4 2377  ralf0 2411  intmin4 2613  iinss 2654  axrep1 2749  axrep2 2750  bm1.3ii 2761  axnul 2764  axpr 2834  ssrel 3304  asymref2 3497  funin 3623  zfrep6 3671  fv3 3790  tfrlem5 3973  dfom3 4692  aceq5 4802  aceq6a 4803  aceq6b 4804  kmlem1 4827  kmlem13 4839  zorn 4859  brdom3 4863  brdom4 4865  axpowndlem2 5015  axacndlem1 5024  axacndlem2 5025  axacndlem3 5026  axacndlem4 5027  axacnd 5029  suppsr2 5288  suppsr3 5289  pre-axsup 5356  peano2nn 5995  islp2 7832  chsscmi 9195  chcmhi 9196  pjnormssi 10179  ref3w 10566  usinuniop 10703

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016

Copyright terms: Public domain