Theorem spi 2207

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

Syntax hints:  ∀wal 1628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-12 2202

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

This theorem is referenced by:  darii  2713  barbari  2715  cesare  2717  camestres  2718  festino  2719  baroco  2720  cesaro  2721  camestros  2722  datisi  2723  disamis  2724  felapton  2727  darapti  2728  calemes  2729  dimatis  2730  fresison  2731  calemos  2732  fesapo  2733  bamalip  2734  kmlem2  9174  axac2  9489  axac  9490  axaci  9491  bnj864  31324