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

Theorem spi 1770
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 1764 . 2  |-  ( A. x ph  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff set class
Syntax hints:   A.wal 1550
This theorem is referenced by:  darii  2382  barbari  2384  cesare  2386  camestres  2387  festino  2388  baroco  2389  cesaro  2390  camestros  2391  datisi  2392  disamis  2393  felapton  2396  darapti  2397  calemes  2398  dimatis  2399  fresison  2400  calemos  2401  fesapo  2402  bamalip  2403  kmlem2  8036  axac2  8351  axac  8352  axaci  8353  bnj864  29367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator