Theorem spi 1560

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

Syntax hints:   A.wal 1371

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

This theorem is referenced by:  19.8a  1614  hbe1a  2052  darii  2155  barbari  2157  cesare  2159  camestres  2160  festino  2161  baroco  2162  cesaro  2163  camestros  2164  datisi  2165  disamis  2166  felapton  2169  darapti  2170  calemes  2171  dimatis  2172  fresison  2173  calemos  2174  fesapo  2175  bamalip  2176  tfi  4635  acexmid  5953  bdsep1  15935  strcoll2  16033  sscoll2  16038