Theorem spi 1470

Description: Inference rule reversing generalization. (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 1441	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
3	1, 2	ax-mp 7	1 ⊢ 𝜑

Syntax hints:  ∀wal 1283

This theorem was proved from axioms:  ax-mp 7  ax-4 1441

This theorem is referenced by:  19.8a  1523  darii  2042  barbari  2044  cesare  2046  camestres  2047  festino  2048  baroco  2049  cesaro  2050  camestros  2051  datisi  2052  disamis  2053  felapton  2056  darapti  2057  calemes  2058  dimatis  2059  fresison  2060  calemos  2061  fesapo  2062  bamalip  2063  tfi  4331  acexmid  5542  bdsep1  10834  strcoll2  10936  sscoll2  10941