Theorem spi 1585

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 1559	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:  ∀wal 1396

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

This theorem is referenced by:  19.8a  1639  hbe1a  2079  darii  2183  barbari  2185  cesare  2187  camestres  2188  festino  2189  baroco  2190  cesaro  2191  camestros  2192  datisi  2193  disamis  2194  felapton  2197  darapti  2198  calemes  2199  dimatis  2200  fresison  2201  calemos  2202  fesapo  2203  bamalip  2204  tfi  4706  acexmid  6051  bdsep1  16704  strcoll2  16802  sscoll2  16807