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

Theorem spi 2219
Description: Inference rule of universal instantiation, or universal specification. Converse of the inference rule of (universal) generalization ax-gen 1877. Contrary to the rule of generalization, its closed form is valid, see sp 2218. (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 2218 . 2 (∀𝑥𝜑𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-12 2214
This theorem depends on definitions:  df-bi 198  df-ex 1860
This theorem is referenced by:  dariiALT  2728  barbariALT  2732  cesareALT  2735  camestresALT  2737  festinoALT  2739  barocoALT  2741  cesaroALT  2743  camestrosALT  2745  datisiOLD  2747  disamisALT  2749  daraptiALT  2753  calemesALT  2756  dimatisOLD  2758  fresisonOLD  2760  calemosOLD  2762  fesapoALT  2764  bamalipOLD  2766  kmlem2  9256  axac2  9571  axac  9572  axaci  9573  bnj864  31313
  Copyright terms: Public domain W3C validator