Theorem 19.21bi 1101

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

Syntax hints:   -> wi 3  A.wal 995

This theorem is referenced by:  19.21bbi 1102  aev 1250  2euex 1484  eqeq1 1528  eleq2 1582  r19.21bi 1772  ssel 2114  pocl 2900  funmo 3589  funeu 3594  funun 3611  fn0 3662  hbfvd2 3788  ac7 4810  axpowndlem2 5015  axpowndlem4 5017  axregndlem2 5020  axinfnd 5023  prcdpq 5162  fipfil2 10658  filint2 10665  cmpmon 10825

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

Copyright terms: Public domain