Theorem spi 1550

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

Syntax hints:  ∀wal 1362

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

This theorem is referenced by:  19.8a  1604  hbe1a  2042  darii  2145  barbari  2147  cesare  2149  camestres  2150  festino  2151  baroco  2152  cesaro  2153  camestros  2154  datisi  2155  disamis  2156  felapton  2159  darapti  2160  calemes  2161  dimatis  2162  fresison  2163  calemos  2164  fesapo  2165  bamalip  2166  tfi  4618  acexmid  5921  bdsep1  15531  strcoll2  15629  sscoll2  15634