Theorem spi 1584

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

Syntax hints:   A.wal 1395

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

This theorem is referenced by:  19.8a  1638  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  4680  acexmid  6016  bdsep1  16480  strcoll2  16578  sscoll2  16583