MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.21bi Structured version   Unicode version

Theorem 19.21bi 1808
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
19.21bi.1  |-  ( ph  ->  A. x ps )
Assertion
Ref Expression
19.21bi  |-  ( ph  ->  ps )

Proof of Theorem 19.21bi
StepHypRef Expression
1 19.21bi.1 . 2  |-  ( ph  ->  A. x ps )
2 sp 1798 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588
This theorem is referenced by:  19.21bbi  1898  equveliOLD  2048  2ax6e  2166  eqeq1dALT  2455  eqeq1OLD  2457  eleq2dALT  2523  eleq2OLD  2527  r19.21bi  2914  elrab3t  3217  ssel  3453  pocl  4751  funmo  5537  funun  5563  fununi  5587  findcard  7657  findcard2  7658  axpowndlem2OLD  8869  axpowndlem4  8872  axregndlem2  8875  axinfnd  8879  prcdnq  9268  relexpindlem  27480  dfrtrcl2  27489  vk15.4j  31546  hbimpg  31576  bnj1379  32137  bnj1052  32279  bnj1118  32288  bnj1154  32303  bnj1280  32324
  Copyright terms: Public domain W3C validator