Theorem spi 1770

Description: Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
spi.1	|- A. x ph

Assertion

Ref	Expression
spi	|- ph

Proof of Theorem spi

Step	Hyp	Ref	Expression
1		spi.1	. 2 |- A. x ph
2		sp 1764	. 2 |- ( A. x ph -> ph )
3	1, 2	ax-mp 5	1 |- ph

Syntax hints:   A.wal 1550

This theorem is referenced by:  darii  2382  barbari  2384  cesare  2386  camestres  2387  festino  2388  baroco  2389  cesaro  2390  camestros  2391  datisi  2392  disamis  2393  felapton  2396  darapti  2397  calemes  2398  dimatis  2399  fresison  2400  calemos  2401  fesapo  2402  bamalip  2403  kmlem2  8036  axac2  8351  axac  8352  axaci  8353  bnj864  29367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762

This theorem depends on definitions:  df-bi 179  df-ex 1552