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

Theorem spi 2167
 Description: Inference rule of universal instantiation, or universal specialization. Converse of the inference rule of (universal) generalization ax-gen 1839. Contrary to the rule of generalization, its closed form is valid, see sp 2166. (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 2166 . 2 (∀𝑥𝜑𝜑)
31, 2ax-mp 5 1 𝜑
 Colors of variables: wff setvar class Syntax hints:  ∀wal 1599 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-12 2162 This theorem depends on definitions:  df-bi 199  df-ex 1824 This theorem is referenced by:  dariiALT  2697  barbariALT  2701  cesareOLD  2704  camestresOLD  2706  festinoALT  2708  barocoALT  2710  cesaroOLD  2712  camestrosOLD  2714  datisiOLD  2716  disamisOLD  2718  daraptiALT  2722  calemesOLD  2725  dimatisOLD  2727  fresisonOLD  2729  calemosOLD  2731  fesapoOLD  2733  bamalipOLD  2735  kmlem2  9308  axac2  9623  axac  9624  axaci  9625  bnj864  31591
 Copyright terms: Public domain W3C validator