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

Theorem 19.21bi 1809
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-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 1799 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797
This theorem depends on definitions:  df-bi 185  df-ex 1592
This theorem is referenced by:  19.21bbi  1891  equveliOLD  2044  2sb6rflem2  2163  eqeq1  2447  eleq2  2502  r19.21bi  2812  elrab3t  3113  ssel  3347  pocl  4644  funmo  5431  funun  5457  fununi  5481  findcard  7547  findcard2  7548  axpowndlem2OLD  8759  axpowndlem4  8762  axregndlem2  8765  axinfnd  8769  prcdnq  9158  relexpindlem  27270  dfrtrcl2  27279  vk15.4j  31066  hbimpg  31096  bnj1379  31658  bnj1052  31800  bnj1118  31809  bnj1154  31824  bnj1280  31845
  Copyright terms: Public domain W3C validator