Theorem spi 1589

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

Syntax hints:  ∀wal 1400

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

This theorem is referenced by:  19.8a  1643  hbe1a  2083  darii  2187  barbari  2189  cesare  2191  camestres  2192  festino  2193  baroco  2194  cesaro  2195  camestros  2196  datisi  2197  disamis  2198  felapton  2201  darapti  2202  calemes  2203  dimatis  2204  fresison  2205  calemos  2206  fesapo  2207  bamalip  2208  tfi  4727  acexmid  6078  bdsep1  16894  strcoll2  16992  sscoll2  16997