Theorem spi 1516

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

Syntax hints:   A.wal 1329

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

This theorem is referenced by:  19.8a  1569  darii  2099  barbari  2101  cesare  2103  camestres  2104  festino  2105  baroco  2106  cesaro  2107  camestros  2108  datisi  2109  disamis  2110  felapton  2113  darapti  2114  calemes  2115  dimatis  2116  fresison  2117  calemos  2118  fesapo  2119  bamalip  2120  tfi  4496  acexmid  5773  bdsep1  13086  strcoll2  13184  sscoll2  13189