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

Theorem 19.21bi 1922
Description: Inference form of 19.21 1962 and also deduction form of sp 1912. (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 1912 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 17 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907
This theorem depends on definitions:  df-bi 188  df-ex 1660
This theorem is referenced by:  19.21bbi  1923  2ax6e  2246  eqeq1dALT  2432  eqeq1OLD  2434  eleq2dALT  2500  eleq2OLD  2504  r19.21biOLD  2802  elrab3t  3234  ssel  3464  pocl  4782  funmo  5617  funun  5643  fununi  5667  findcard  7816  findcard2  7817  axpowndlem4  9023  axregndlem2  9026  axinfnd  9030  prcdnq  9417  dfrtrcl2  13104  relexpindlem  13105  bnj1379  29430  bnj1052  29572  bnj1118  29581  bnj1154  29596  bnj1280  29617  dftrcl3  35951  dfrtrcl3  35964  vk15.4j  36522  hbimpg  36558
  Copyright terms: Public domain W3C validator