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

Syntax hints:  ∀wal 1329

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

This theorem is referenced by:  19.8a  1569  darii  2097  barbari  2099  cesare  2101  camestres  2102  festino  2103  baroco  2104  cesaro  2105  camestros  2106  datisi  2107  disamis  2108  felapton  2111  darapti  2112  calemes  2113  dimatis  2114  fresison  2115  calemos  2116  fesapo  2117  bamalip  2118  tfi  4491  acexmid  5766  bdsep1  13072  strcoll2  13170  sscoll2  13175