Theorem exim 1530

Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-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		hba1 1473	. 2 |- ( A. x ( ph -> ps ) -> A. x A. x ( ph -> ps ) )
2		hbe1 1424	. 2 |- ( E. x ps -> A. x E. x ps )
3		19.8a 1522	. . . 4 |- ( ps -> E. x ps )
4	3	imim2i 12	. . 3 |- ( ( ph -> ps ) -> ( ph -> E. x ps ) )
5	4	sps 1470	. 2 |- ( A. x ( ph -> ps ) -> ( ph -> E. x ps ) )
6	1, 2, 5	exlimdh 1527	1 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )

Syntax hints:   -> wi 4   A.wal 1282   E.wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-ial 1467

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  eximi  1531  exbi  1535  eximdh  1542  19.29  1551  19.25  1557  alexim  1576  19.23t  1607  spimt  1664  equvini  1681  nfexd  1684  ax10oe  1718  sbcof2  1731  spsbim  1764  mor  1983  rexim  2455  elex22  2614  elex2  2615  vtoclegft  2670  spcimgft  2674  spcimegft  2676  spc2gv  2688  spc3gv  2690  ssoprab2  5581  bj-inf2vnlem1  10765