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

Theorem 19.21bi 1818
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 1808 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  19.21bbi  1908  equveliOLD  2062  2ax6e  2180  eqeq1dALT  2470  eqeq1OLD  2472  eleq2dALT  2538  eleq2OLD  2542  r19.21biOLD  2834  elrab3t  3260  ssel  3498  pocl  4807  funmo  5604  funun  5630  fununi  5654  findcard  7759  findcard2  7760  axpowndlem2OLD  8974  axpowndlem4  8977  axregndlem2  8980  axinfnd  8984  prcdnq  9371  relexpindlem  28565  dfrtrcl2  28574  vk15.4j  32395  hbimpg  32425  bnj1379  32986  bnj1052  33128  bnj1118  33137  bnj1154  33152  bnj1280  33173
  Copyright terms: Public domain W3C validator