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  2077  darii  2181  barbari  2183  cesare  2185  camestres  2186  festino  2187  baroco  2188  cesaro  2189  camestros  2190  datisi  2191  disamis  2192  felapton  2195  darapti  2196  calemes  2197  dimatis  2198  fresison  2199  calemos  2200  fesapo  2201  bamalip  2202  tfi  4703  acexmid  6048  bdsep1  16642  strcoll2  16740  sscoll2  16745