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

Theorem spi 1738
Description: Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
spi.1  |-  A. x ph
Assertion
Ref Expression
spi  |-  ph

Proof of Theorem spi
StepHypRef Expression
1 spi.1 . 2  |-  A. x ph
2 sp 1716 . 2  |-  ( A. x ph  ->  ph )
31, 2ax-mp 8 1  |-  ph
Colors of variables: wff set class
Syntax hints:   A.wal 1527
This theorem is referenced by:  darii  2242  barbari  2244  cesare  2246  camestres  2247  festino  2248  baroco  2249  cesaro  2250  camestros  2251  datisi  2252  disamis  2253  felapton  2256  darapti  2257  calemes  2258  dimatis  2259  fresison  2260  calemos  2261  fesapo  2262  bamalip  2263  kmlem2  7777  axac2  8093  axac  8094  axaci  8095  ballotlem2  23047  axlmp2  25025  axlmp3  25026  bnj864  28954
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
  Copyright terms: Public domain W3C validator