Theorem exim 1633

Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)

Assertion

Ref	Expression
exim	|- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )

Proof of Theorem exim

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ( ph -> ps ) -> ( ph -> ps ) )
2	1	aleximi 1632	1 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )

Syntax hints:   -> wi 4   A.wal 1377   E.wex 1596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612

This theorem depends on definitions:  df-bi 185  df-ex 1597

This theorem is referenced by:  eximi  1635  aleximiOLD  1638  19.8a  1806  19.8aOLD  1807  19.9ht  1837  19.23t  1856  19.23v  1932  spimt  1974  2moOLDOLD  2384  elex2  3130  elex22  3131  vtoclegft  3190  spcimgft  3194  2exim  31186  pm11.71  31205  onfrALTlem2  32799  19.41rg  32804  ax6e2nd  32812  elex2VD  33119  elex22VD  33120  onfrALTlem2VD  33170  19.41rgVD  33183  ax6e2eqVD  33188  ax6e2ndVD  33189  ax6e2ndeqVD  33190  ax6e2ndALT  33211  ax6e2ndeqALT  33212  bj-axdd2  33663  bj-2exim  33691  bj-exlimh  33700  bj-alequex  33751  bj-spimtv  33761