Theorem spi 1584

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

Syntax hints:  ∀wal 1395

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

This theorem is referenced by:  19.8a  1638  hbe1a  2075  darii  2179  barbari  2181  cesare  2183  camestres  2184  festino  2185  baroco  2186  cesaro  2187  camestros  2188  datisi  2189  disamis  2190  felapton  2193  darapti  2194  calemes  2195  dimatis  2196  fresison  2197  calemos  2198  fesapo  2199  bamalip  2200  tfi  4682  acexmid  6022  bdsep1  16540  strcoll2  16638  sscoll2  16643