Theorem spi 1562

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

Syntax hints:  ∀wal 1373

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

This theorem is referenced by:  19.8a  1616  hbe1a  2054  darii  2158  barbari  2160  cesare  2162  camestres  2163  festino  2164  baroco  2165  cesaro  2166  camestros  2167  datisi  2168  disamis  2169  felapton  2172  darapti  2173  calemes  2174  dimatis  2175  fresison  2176  calemos  2177  fesapo  2178  bamalip  2179  tfi  4651  acexmid  5973  bdsep1  16158  strcoll2  16256  sscoll2  16261