Theorem 19.21ai 998

Description: Inference from Theorem 19.21 of [Margaris] p. 90.

Hypotheses

Ref	Expression
19.21ai.1	|- (ph -> A.xph)
19.21ai.2	|- (ph -> ps)

Assertion

Ref	Expression
19.21ai	|- (ph -> A.xps)

Proof of Theorem 19.21ai

Step	Hyp	Ref	Expression
1		19.21ai.1	. 2 |- (ph -> A.xph)
2		19.21ai.2	. . 3 |- (ph -> ps)
3	2	19.20i 992	. 2 |- (A.xph -> A.xps)
4	1, 3	syl 10	1 |- (ph -> A.xps)

Syntax hints:   -> wi 3  A.wal 954

This theorem is referenced by:  hbim 1007  19.12 1047  19.21 1056  19.21ad 1059  19.22d 1062  19.23 1063  19.23ad 1066  19.38 1081  nexd 1102  albid 1104  exbid 1105  hbnd 1109  ax11i 1138  sb6x 1188  equs5e 1198  aev 1208  sbbid 1246  dvelimdf 1251  sb6rf 1260  sb8 1261  a16g 1276  19.21aiv 1286  ax11f 1365  ax11indalem 1368  ax11inda2ALT 1369  a12lem1 1376  2moex 1440  2mo 1447  abbid 1576  r19.21ai 1712  ceqsalg 1825  ceqsex 1834  sbcbid 1976  csbeq2d 2018  hbcsb1g 2024  hbcsbg 2026  csbnestglem 2035  csbnest1g 2037  zfrepclf 2699  ssopab2 2822  dmcosseq 3365  imadif 3574  fnopabg 3615  hbfvd2 3731  axrepnd 4946  axunnd 4948  axpownd 4953  axregndlem1 4954  axacndlem1 4959  axacndlem2 4960  axacndlem3 4961  axacndlem4 4962  axacndlem5 4963  axacnd 4964  suppsr3 5224  chcmh 9113  homcard 10539  imonclem 10741  ismonc 10742

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