Theorem spi 1582

Description: Inference reversing generalization (specialization). (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		ax-4 1556	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:  ∀wal 1393

This theorem was proved from axioms:  ax-mp 5  ax-4 1556

This theorem is referenced by:  19.8a  1636  hbe1a  2074  darii  2178  barbari  2180  cesare  2182  camestres  2183  festino  2184  baroco  2185  cesaro  2186  camestros  2187  datisi  2188  disamis  2189  felapton  2192  darapti  2193  calemes  2194  dimatis  2195  fresison  2196  calemos  2197  fesapo  2198  bamalip  2199  tfi  4674  acexmid  6006  bdsep1  16272  strcoll2  16370  sscoll2  16375