Theorem spi 1585

Description: Inference reversing generalization (specialization). (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		ax-4 1559	. 2 |- ( A. x ph -> ph )
3	1, 2	ax-mp 5	1 |- ph

Syntax hints:   A.wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-4 1559

This theorem is referenced by:  19.8a  1639  hbe1a  2076  darii  2180  barbari  2182  cesare  2184  camestres  2185  festino  2186  baroco  2187  cesaro  2188  camestros  2189  datisi  2190  disamis  2191  felapton  2194  darapti  2195  calemes  2196  dimatis  2197  fresison  2198  calemos  2199  fesapo  2200  bamalip  2201  tfi  4686  acexmid  6027  bdsep1  16584  strcoll2  16682  sscoll2  16687