Theorem 19.21bi 742

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

Syntax hints:   -> wi 2  A.wal 672

This theorem is referenced by:  19.21bbi 743  2euex 1061  cleq1 1107  eleq2 1150  r19.21bi 1266  ssel 1502  pocl 2132  funmo 2680  funeu 2685  funun 2700  fn0 2739  axpowndlem2 3744  axpowndlem4 3746  axregndlem2 3749  axinfnd 3752  prcdpq 3891

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6  ax-4 673

metamath.org