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

Theorem spi 1765
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 1759 . 2  |-  ( A. x ph  ->  ph )
31, 2ax-mp 8 1  |-  ph
Colors of variables: wff set class
Syntax hints:   A.wal 1546
This theorem is referenced by:  darii  2361  barbari  2363  cesare  2365  camestres  2366  festino  2367  baroco  2368  cesaro  2369  camestros  2370  datisi  2371  disamis  2372  felapton  2375  darapti  2376  calemes  2377  dimatis  2378  fresison  2379  calemos  2380  fesapo  2381  bamalip  2382  kmlem2  7995  axac2  8310  axac  8311  axaci  8312  bnj864  29011
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator