Theorem spi 1516

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

Syntax hints:  ∀wal 1333

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

This theorem is referenced by:  19.8a  1570  hbe1a  2003  darii  2106  barbari  2108  cesare  2110  camestres  2111  festino  2112  baroco  2113  cesaro  2114  camestros  2115  datisi  2116  disamis  2117  felapton  2120  darapti  2121  calemes  2122  dimatis  2123  fresison  2124  calemos  2125  fesapo  2126  bamalip  2127  tfi  4541  acexmid  5823  bdsep1  13471  strcoll2  13569  sscoll2  13574