Theorem spi 2054

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

Syntax hints:  ∀wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

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

This theorem is referenced by:  darii  2565  barbari  2567  cesare  2569  camestres  2570  festino  2571  baroco  2572  cesaro  2573  camestros  2574  datisi  2575  disamis  2576  felapton  2579  darapti  2580  calemes  2581  dimatis  2582  fresison  2583  calemos  2584  fesapo  2585  bamalip  2586  kmlem2  8973  axac2  9288  axac  9289  axaci  9290  bnj864  30992