Theorem spi 1469

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

Syntax hints:  ∀wal 1282

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

This theorem is referenced by:  19.8a  1522  darii  2041  barbari  2043  cesare  2045  camestres  2046  festino  2047  baroco  2048  cesaro  2049  camestros  2050  datisi  2051  disamis  2052  felapton  2055  darapti  2056  calemes  2057  dimatis  2058  fresison  2059  calemos  2060  fesapo  2061  bamalip  2062  tfi  4323  acexmid  5531  bdsep1  10676  strcoll2  10778  sscoll2  10783