Theorem 19.21ai 974

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 968	. 2 |- (A.xph -> A.xps)
4	1, 3	syl 10	1 |- (ph -> A.xps)

Syntax hints:   -> wi 3  A.wal 950

This theorem is referenced by:  hbim 983  19.12 1023  19.21 1032  19.21ad 1035  19.22d 1038  19.23 1039  19.23ad 1042  19.38 1057  nexd 1078  albid 1080  exbid 1081  hbnd 1085  sb6x 1171  equs5e 1182  aev 1192  sbbid 1230  dvelimdf 1235  sb6rf 1244  sb8 1245  a16g 1258  19.21aiv 1268  ax11f 1342  ax11indalem 1345  ax11inda2ALT 1346  a12lem1 1353  2moex 1417  2mo 1424  abbid 1552  r19.21ai 1688  ceqsalg 1800  ceqsex 1809  sbcbid 1947  csbeq2d 1989  hbcsb1g 1995  hbcsbg 1997  csbnestglem 2006  csbnest1g 2008  zfrepclf 2667  ssopab2 2784  dmcosseq 3316  imadif 3514  fnopabg 3555  hbfvd2 3670  axrepnd 4869  axunnd 4871  axpownd 4876  axregndlem1 4877  axacndlem1 4882  axacndlem2 4883  axacndlem3 4884  axacndlem4 4885  axacndlem5 4886  axacnd 4887  suppsr3 5147  imonclem 8933  ismonc 8934  chcmh 9264

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-4 951  ax-5 952  ax-gen 955

Copyright terms: Public domain