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

Step	Hyp	Ref	Expression
1		spi.1	. 2 ⊢ ∀𝑥𝜑
2		sp 2166	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

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