HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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
StepHypRef Expression
1 19.21bi.1 . 2 |- (ph -> A.xps)
2 ax-4 1319 . 2 |- (A.xps -> ps)
31, 2syl 12 1 |- (ph -> ps)
Colors of variables: wff set class
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