Theorem spi 1429

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

Syntax hints:   A.wal 1241

This theorem was proved from axioms:  ax-mp 7  ax-4 1400

This theorem is referenced by:  19.8a  1482  darii  2000  barbari  2002  cesare  2004  camestres  2005  festino  2006  baroco  2007  cesaro  2008  camestros  2009  datisi  2010  disamis  2011  felapton  2014  darapti  2015  calemes  2016  dimatis  2017  fresison  2018  calemos  2019  fesapo  2020  bamalip  2021  tfi  4305  acexmid  5511  bdsep1  10005  strcoll2  10108  sscoll2  10113