Theorem spi 1524

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

Syntax hints:  ∀wal 1341

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

This theorem is referenced by:  19.8a  1578  hbe1a  2011  darii  2114  barbari  2116  cesare  2118  camestres  2119  festino  2120  baroco  2121  cesaro  2122  camestros  2123  datisi  2124  disamis  2125  felapton  2128  darapti  2129  calemes  2130  dimatis  2131  fresison  2132  calemos  2133  fesapo  2134  bamalip  2135  tfi  4559  acexmid  5841  bdsep1  13767  strcoll2  13865  sscoll2  13870