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

Theorem spi 1759
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 1753 . 2  |-  ( A. x ph  ->  ph )
31, 2ax-mp 8 1  |-  ph
Colors of variables: wff set class
Syntax hints:   A.wal 1545
This theorem is referenced by:  darii  2316  barbari  2318  cesare  2320  camestres  2321  festino  2322  baroco  2323  cesaro  2324  camestros  2325  datisi  2326  disamis  2327  felapton  2330  darapti  2331  calemes  2332  dimatis  2333  fresison  2334  calemos  2335  fesapo  2336  bamalip  2337  kmlem2  7924  axac2  8240  axac  8241  axaci  8242  ballotlem2  24315  bnj864  28706
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751
This theorem depends on definitions:  df-bi 177  df-ex 1547
  Copyright terms: Public domain W3C validator