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