Theorem spi 1560

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

Syntax hints:  ∀wal 1371

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

This theorem is referenced by:  19.8a  1614  hbe1a  2052  darii  2155  barbari  2157  cesare  2159  camestres  2160  festino  2161  baroco  2162  cesaro  2163  camestros  2164  datisi  2165  disamis  2166  felapton  2169  darapti  2170  calemes  2171  dimatis  2172  fresison  2173  calemos  2174  fesapo  2175  bamalip  2176  tfi  4634  acexmid  5950  bdsep1  15895  strcoll2  15993  sscoll2  15998