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 ⊢ 𝜑

This proof depends on syntax axioms:  ∀wal 1400

This proof depends on axioms:  ax-mp 5  ax-4 1563

This theorem is used 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  4729  acexmid  6084  bdsep1  16923  strcoll2  17021  sscoll2  17026