Theorem spi 1536

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

Syntax hints:  ∀wal 1351

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

This theorem is referenced by:  19.8a  1590  hbe1a  2023  darii  2126  barbari  2128  cesare  2130  camestres  2131  festino  2132  baroco  2133  cesaro  2134  camestros  2135  datisi  2136  disamis  2137  felapton  2140  darapti  2141  calemes  2142  dimatis  2143  fresison  2144  calemos  2145  fesapo  2146  bamalip  2147  tfi  4583  acexmid  5876  bdsep1  14722  strcoll2  14820  sscoll2  14825