Theorem spi 1529

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

Syntax hints:  ∀wal 1346

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

This theorem is referenced by:  19.8a  1583  hbe1a  2016  darii  2119  barbari  2121  cesare  2123  camestres  2124  festino  2125  baroco  2126  cesaro  2127  camestros  2128  datisi  2129  disamis  2130  felapton  2133  darapti  2134  calemes  2135  dimatis  2136  fresison  2137  calemos  2138  fesapo  2139  bamalip  2140  tfi  4566  acexmid  5852  bdsep1  13920  strcoll2  14018  sscoll2  14023