Theorem 19.21bi 1060

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

Hypothesis

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

Assertion

Ref	Expression
19.21bi	|- (ph -> ps)

Proof of Theorem 19.21bi

Step	Hyp	Ref	Expression
1		19.21bi.1	. 2 |- (ph -> A.xps)
2		ax-4 973	. 2 |- (A.xps -> ps)
3	1, 2	syl 10	1 |- (ph -> ps)

Syntax hints:   -> wi 3  A.wal 954

This theorem is referenced by:  19.21bbi 1061  aev 1208  2euex 1441  eqeq1 1481  eleq2 1535  r19.21bi 1725  ssel 2063  pocl 2844  funmo 3532  funeu 3537  funun 3554  fn0 3605  hbfvd2 3731  ac7 4748  axpowndlem2 4950  axpowndlem4 4952  axregndlem2 4955  axinfnd 4958  prcdpq 5097  fillsb 10560  fipfil2 10564  fipfil2OLD 10565  filint2 10574  filint2OLD 10575  cmpmon 10743

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

Copyright terms: Public domain