Metamath Proof Explorer

Theorem spi

Description: Inference rule of universal instantiation, or universal specialization. Converse of the inference rule of (universal) generalization ax-gen . Contrary to the rule of generalization, its closed form is valid, see sp . (Contributed by NM, 5-Aug-1993)

Ref Expression
Hypothesis spi.1 x φ
Assertion spi φ


Step Hyp Ref Expression
1 spi.1 x φ
2 sp x φ φ
3 1 2 ax-mp φ