Theorem spi 1765

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 1759	. 2 |- ( A. x ph -> ph )
3	1, 2	ax-mp 8	1 |- ph

Syntax hints:   A.wal 1546

This theorem is referenced by:  darii  2361  barbari  2363  cesare  2365  camestres  2366  festino  2367  baroco  2368  cesaro  2369  camestros  2370  datisi  2371  disamis  2372  felapton  2375  darapti  2376  calemes  2377  dimatis  2378  fresison  2379  calemos  2380  fesapo  2381  bamalip  2382  kmlem2  7995  axac2  8310  axac  8311  axaci  8312  bnj864  29011

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-ex 1548