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

Theorem spi 1813
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 1808 . 2  |-  ( A. x ph  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:   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:  darii  2408  barbari  2410  cesare  2412  camestres  2413  festino  2414  baroco  2415  cesaro  2416  camestros  2417  datisi  2418  disamis  2419  felapton  2422  darapti  2423  calemes  2424  dimatis  2425  fresison  2426  calemos  2427  fesapo  2428  bamalip  2429  kmlem2  8543  axac2  8858  axac  8859  axaci  8860  bnj864  33460
  Copyright terms: Public domain W3C validator