Theorem 19.21ai 997

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

Syntax hints:   -> wi 3  A.wal 953

This theorem is referenced by:  hbim 1006  19.12 1046  19.21 1055  19.21ad 1058  19.22d 1061  19.23 1062  19.23ad 1065  19.38 1080  nexd 1101  albid 1103  exbid 1104  hbnd 1108  ax11i 1137  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 1575  r19.21ai 1711  ceqsalg 1823  ceqsex 1832  sbcbid 1974  csbeq2d 2016  hbcsb1g 2022  hbcsbg 2024  csbnestglem 2033  csbnest1g 2035  zfrepclf 2696  ssopab2 2819  dmcosseq 3362  imadif 3571  fnopabg 3612  hbfvd2 3728  axrepnd 4933  axunnd 4935  axpownd 4940  axregndlem1 4941  axacndlem1 4946  axacndlem2 4947  axacndlem3 4948  axacndlem4 4949  axacndlem5 4950  axacnd 4951  suppsr3 5211  chcmh 9101  homcard 10520  imonclem 10690  ismonc 10691

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974

Copyright terms: Public domain