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

Theorem spi 2052
Description: Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
spi.1 𝑥𝜑
Assertion
Ref Expression
spi 𝜑

Proof of Theorem spi
StepHypRef Expression
1 spi.1 . 2 𝑥𝜑
2 sp 2051 . 2 (∀𝑥𝜑𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  darii  2564  barbari  2566  cesare  2568  camestres  2569  festino  2570  baroco  2571  cesaro  2572  camestros  2573  datisi  2574  disamis  2575  felapton  2578  darapti  2579  calemes  2580  dimatis  2581  fresison  2582  calemos  2583  fesapo  2584  bamalip  2585  kmlem2  8917  axac2  9232  axac  9233  axaci  9234  bnj864  30700
  Copyright terms: Public domain W3C validator