Theorem 19.20i 992

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

Syntax hints:   -> wi 3  A.wal 954

This theorem is referenced by:  19.20i2 993  19.20 994  19.20ii 995  19.21ai 998  hbal 1005  ax67 1020  ax67to6 1021  ax67to7 1022  ax467 1023  ax467to6 1025  ax467to7 1026  19.9d 1037  19.18 1050  19.26 1067  19.25 1084  19.33 1091  19.33b 1092  hbimd 1110  19.21t 1115  equid 1126  ax10 1141  a4im 1159  stdpc4 1185  sbied 1195  aev 1208  ax11 1219  hbsb4 1248  sbco3 1257  sbcom 1258  sb9i 1263  ax16i 1270  sbal1 1346  sbal2 1358  ax11eq 1363  ax11el 1364  ax11indi 1367  a12stdy3 1374  a12study 1378  mo 1393  eumo0 1395  mo2 1400  2mo 1447  bm1.1 1462  alral 1692  rgen2a 1699  r19.20i2 1703  r19.27av 1754  ceqsalg 1825  elabgt 1895  reu3 1931  sbciegft 1959  csbexg 2008  csbiegft 2029  csbnestg 2036  sbcnestg 2038  rabss2 2129  unss1 2199  ssrin 2234  undif4 2325  ralf0 2359  intmin4 2559  iinss 2600  axrep1 2694  axrep2 2695  bm1.3ii 2706  axnul 2709  axpr 2778  ssrel 3247  asymref2 3440  funin 3566  zfrep6 3614  fv3 3733  tfrlem5 3915  dfom3 4630  aceq5 4740  aceq6a 4741  aceq6b 4742  kmlem1 4765  kmlem13 4777  zorn 4797  brdom3 4801  brdom4 4803  axpowndlem2 4950  axacndlem1 4959  axacndlem2 4960  axacndlem3 4961  axacndlem4 4962  axacnd 4964  suppsr2 5223  suppsr3 5224  pre-axsup 5291  peano2nn 5935  islp2 7747  chsscm 9112  chcmh 9113  pjnormss 10096

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975

Copyright terms: Public domain