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

Theorem spi 1804
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 1799 . 2  |-  ( A. x ph  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:   A.wal 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797
This theorem depends on definitions:  df-bi 185  df-ex 1592
This theorem is referenced by:  darii  2385  barbari  2387  cesare  2389  camestres  2390  festino  2391  baroco  2392  cesaro  2393  camestros  2394  datisi  2395  disamis  2396  felapton  2399  darapti  2400  calemes  2401  dimatis  2402  fresison  2403  calemos  2404  fesapo  2405  bamalip  2406  kmlem2  8316  axac2  8631  axac  8632  axaci  8633  bnj864  31749
  Copyright terms: Public domain W3C validator