Theorem 19.20i 994

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

Syntax hints:   -> wi 3  A.wal 956

This theorem is referenced by:  19.20i2 995  19.20 996  19.20ii 997  19.21ai 1000  hbal 1007  ax67 1022  ax67to6 1023  ax67to7 1024  ax467 1025  ax467to6 1027  ax467to7 1028  19.9d 1039  19.18 1052  19.26 1069  19.25 1086  19.33 1093  19.33b 1094  hbimd 1112  19.21t 1117  equid 1128  ax10 1143  a4im 1161  stdpc4 1187  sbied 1197  aev 1210  ax11 1221  hbsb4 1250  sbco3 1259  sbcom 1260  sb9i 1265  ax16i 1272  sbal1 1348  sbal2 1360  ax11eq 1365  ax11el 1366  ax11indi 1369  a12stdy3 1376  a12study 1380  mo 1395  eumo0 1397  mo2 1402  2mo 1450  bm1.1 1465  alral 1695  rgen2a 1702  r19.20i2 1706  r19.27av 1757  ceqsalg 1828  elabgt 1898  reu3 1934  sbciegft 1963  csbexg 2012  csbiegft 2033  csbnestg 2040  sbcnestg 2042  rabss2 2133  unss1 2203  ssrin 2238  undif4 2330  ralf0 2364  intmin4 2564  iinss 2605  axrep1 2700  axrep2 2701  bm1.3ii 2712  axnul 2715  axpr 2785  ssrel 3254  asymref2 3447  funin 3573  zfrep6 3621  fv3 3740  tfrlem5 3922  dfom3 4646  aceq5 4757  aceq6a 4758  aceq6b 4759  kmlem1 4782  kmlem13 4794  zorn 4814  brdom3 4818  brdom4 4820  axpowndlem2 4969  axacndlem1 4978  axacndlem2 4979  axacndlem3 4980  axacndlem4 4981  axacnd 4983  suppsr2 5242  suppsr3 5243  pre-axsup 5310  peano2nn 5944  islp2 7751  chsscm 9114  chcmh 9115  pjnormss 10098

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

Copyright terms: Public domain