Theorem spi 1547

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

Syntax hints:   A.wal 1362

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

This theorem is referenced by:  19.8a  1601  hbe1a  2039  darii  2142  barbari  2144  cesare  2146  camestres  2147  festino  2148  baroco  2149  cesaro  2150  camestros  2151  datisi  2152  disamis  2153  felapton  2156  darapti  2157  calemes  2158  dimatis  2159  fresison  2160  calemos  2161  fesapo  2162  bamalip  2163  tfi  4614  acexmid  5917  bdsep1  15377  strcoll2  15475  sscoll2  15480