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

Theorem 19.21bi 1958
Description: Inference form of 19.21 1998 and also deduction form of sp 1948. (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 1948 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 17 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-12 1944
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675
This theorem is referenced by:  19.21bbi  1959  2ax6e  2290  eqeq1dALT  2465  eleq2dALT  2527  r19.21biOLD  2770  elrab3t  3207  ssel  3438  pocl  4781  funmo  5617  funun  5643  fununi  5671  findcard  7836  findcard2  7837  axpowndlem4  9051  axregndlem2  9054  axinfnd  9057  prcdnq  9444  dfrtrcl2  13174  relexpindlem  13175  bnj1379  29691  bnj1052  29833  bnj1118  29842  bnj1154  29857  bnj1280  29878  dftrcl3  36357  dfrtrcl3  36370  vk15.4j  36929  hbimpg  36965
  Copyright terms: Public domain W3C validator