Theorem spi 2042

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

Syntax hints:  ∀wal 1473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  darii  2553  barbari  2555  cesare  2557  camestres  2558  festino  2559  baroco  2560  cesaro  2561  camestros  2562  datisi  2563  disamis  2564  felapton  2567  darapti  2568  calemes  2569  dimatis  2570  fresison  2571  calemos  2572  fesapo  2573  bamalip  2574  kmlem2  8856  axac2  9171  axac  9172  axaci  9173  bnj864  30246