Theorem spi 2053

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

Syntax hints:  ∀wal 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-12 2046

This theorem depends on definitions:  df-bi 197  df-ex 1704

This theorem is referenced by:  darii  2564  barbari  2566  cesare  2568  camestres  2569  festino  2570  baroco  2571  cesaro  2572  camestros  2573  datisi  2574  disamis  2575  felapton  2578  darapti  2579  calemes  2580  dimatis  2581  fresison  2582  calemos  2583  fesapo  2584  bamalip  2585  kmlem2  8970  axac2  9285  axac  9286  axaci  9287  bnj864  30977