Theorem 19.21bi 1058

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

Syntax hints:   -> wi 3  A.wal 952

This theorem is referenced by:  19.21bbi 1059  aev 1206  2euex 1439  eqeq1 1478  eleq2 1532  r19.21bi 1722  ssel 2059  pocl 2839  funmo 3524  funeu 3529  funun 3546  fn0 3597  hbfvd2 3722  ac7 4728  axpowndlem2 4930  axpowndlem4 4932  axregndlem2 4935  axinfnd 4938  prcdpq 5077  fillsb 10471  fipfil2 10475  filint2 10482  cmpmon 10621

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

Copyright terms: Public domain