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

Theorem spi 2207
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 2206 . 2 (∀𝑥𝜑𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-12 2202
This theorem depends on definitions:  df-bi 197  df-ex 1852
This theorem is referenced by:  darii  2713  barbari  2715  cesare  2717  camestres  2718  festino  2719  baroco  2720  cesaro  2721  camestros  2722  datisi  2723  disamis  2724  felapton  2727  darapti  2728  calemes  2729  dimatis  2730  fresison  2731  calemos  2732  fesapo  2733  bamalip  2734  kmlem2  9174  axac2  9489  axac  9490  axaci  9491  bnj864  31324
  Copyright terms: Public domain W3C validator