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

Theorem spi 1799
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 1794 . 2  |-  ( A. x ph  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:   A.wal 1367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-ex 1587
This theorem is referenced by:  darii  2386  barbari  2388  cesare  2390  camestres  2391  festino  2392  baroco  2393  cesaro  2394  camestros  2395  datisi  2396  disamis  2397  felapton  2400  darapti  2401  calemes  2402  dimatis  2403  fresison  2404  calemos  2405  fesapo  2406  bamalip  2407  kmlem2  8320  axac2  8635  axac  8636  axaci  8637  bnj864  31915
  Copyright terms: Public domain W3C validator