Theorem 19.21bi 1408

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

Syntax hints:   -> wi 3  A.wal 1296

This theorem is referenced by:  19.21bbi 1409  aevOLD 1578  2euexOLD 1845  eqeq1 1890  eleq2 1958  r19.21bi 2188  ssel 2615  pocl 3596  eualeqhb 3824  euexeqOLD 3826  funmo 4437  funeuOLD 4445  funun 4462  fn0OLD 4533  hbfvd2 4688  ac7 5910  axpowndlem2 6102  axpowndlem4 6104  axregndlem2 6107  axinfnd 6110  prcdpq 6249  findcard 10178  fipfil2 10272  bnj23 12397  bnj1285 13036  bnj1379 13100  bnj1052 13395  bnj1118 13420  bnj1154 13438  bnj1284 13482  imfstnrelc 14396  filint2 14923  cmpmon 15164  finsschain 15373  fcluscomplem 15620  findcard2 15745  ersym2 16256  ertr2 16257  prtlem18 16279

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

Copyright terms: Public domain