Theorem spi 1546

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

Syntax hints:  ∀wal 1361

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

This theorem is referenced by:  19.8a  1600  hbe1a  2033  darii  2136  barbari  2138  cesare  2140  camestres  2141  festino  2142  baroco  2143  cesaro  2144  camestros  2145  datisi  2146  disamis  2147  felapton  2150  darapti  2151  calemes  2152  dimatis  2153  fresison  2154  calemos  2155  fesapo  2156  bamalip  2157  tfi  4593  acexmid  5887  bdsep1  14933  strcoll2  15031  sscoll2  15036