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 4740  axpowndlem2 4942  axpowndlem4 4944  axregndlem2 4947  axinfnd 4950  prcdpq 5089  fillsb 10520  fipfil2 10524  filint2 10531  cmpmon 10684

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

Copyright terms: Public domain