Theorem spi 1517

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

Syntax hints:  ∀wal 1330

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

This theorem is referenced by:  19.8a  1570  darii  2100  barbari  2102  cesare  2104  camestres  2105  festino  2106  baroco  2107  cesaro  2108  camestros  2109  datisi  2110  disamis  2111  felapton  2114  darapti  2115  calemes  2116  dimatis  2117  fresison  2118  calemos  2119  fesapo  2120  bamalip  2121  tfi  4504  acexmid  5781  bdsep1  13254  strcoll2  13352  sscoll2  13357