Theorem spi 1547

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

Syntax hints:  ∀wal 1362

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

This theorem is referenced by:  19.8a  1601  hbe1a  2035  darii  2138  barbari  2140  cesare  2142  camestres  2143  festino  2144  baroco  2145  cesaro  2146  camestros  2147  datisi  2148  disamis  2149  felapton  2152  darapti  2153  calemes  2154  dimatis  2155  fresison  2156  calemos  2157  fesapo  2158  bamalip  2159  tfi  4596  acexmid  5891  bdsep1  15041  strcoll2  15139  sscoll2  15144