Theorem 19.20i 1028

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

Syntax hints:   -> wi 3  A.wal 990

This theorem is referenced by:  19.20i2 1029  19.20 1030  19.20ii 1031  19.21ai 1034  hbal 1041  ax67 1056  ax67to6 1057  ax67to7 1058  ax467 1059  ax467to6 1061  ax467to7 1062  19.9d 1073  19.18 1086  19.26 1103  19.25 1120  19.33 1127  19.33b 1128  hbimd 1146  19.21t 1151  equid 1162  ax10 1178  a4im 1196  stdpc4 1222  sbied 1232  aev 1245  ax11 1256  hbsb4 1286  sbco3 1295  sbcom 1296  sb9i 1301  ax16i 1308  sbal1 1385  sbal2 1397  ax11eq 1402  ax11el 1403  ax11indi 1406  a12stdy3 1413  a12study 1417  mo 1432  eumo0 1434  mo2 1439  2mo 1487  bm1.1 1504  alral 1738  rgen2a 1745  r19.20i2 1749  r19.27av 1800  ceqsalg 1871  elabgt 1941  reu3 1977  sbciegft 2007  csbexg 2059  csbiegft 2081  csbnestg 2088  sbcnestg 2090  rabss2 2181  unss1 2251  ssrin 2286  undif4 2378  ralf0 2413  intmin4 2626  iinss 2668  axrep1 2768  axrep2 2769  bm1.3ii 2780  axnul 2783  axpr 2854  ssrel 3334  ssrelrel 3340  asymref2 3532  funin 3671  zfrep6 3721  fv3 3844  tfrlem5 4216  dfom3 4776  aceq5 4886  aceq6a 4887  aceq6b 4888  kmlem1 4911  kmlem13 4923  zorn 4943  brdom3 4947  brdom4 4949  axpowndlem2 5104  axacndlem1 5113  axacndlem2 5114  axacndlem3 5115  axacndlem4 5116  axacnd 5118  suppsr2 5377  suppsr3 5378  pre-axsup 5445  peano2nn 6080  islp2 7957  chsscmi 9388  chcmhi 9389  pjnormssi 10376  ref3w 10772  inttr 10787  usinuniop 11128  dfiin2g 11400  nninfnub 11882

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 999  ax-4 1009  ax-5o 1011

Copyright terms: Public domain