Theorem exim 1579

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 1521	. 2 |- ( A. x ( ph -> ps ) -> A. x A. x ( ph -> ps ) )
2		hbe1 1472	. 2 |- ( E. x ps -> A. x E. x ps )
3		19.8a 1570	. . . 4 |- ( ps -> E. x ps )
4	3	imim2i 12	. . 3 |- ( ( ph -> ps ) -> ( ph -> E. x ps ) )
5	4	sps 1518	. 2 |- ( A. x ( ph -> ps ) -> ( ph -> E. x ps ) )
6	1, 2, 5	exlimdh 1576	1 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )

Syntax hints:   -> wi 4   A.wal 1330   E.wex 1469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-ial 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eximi  1580  exbi  1584  eximdh  1591  19.29  1600  19.25  1606  alexim  1625  19.23t  1656  spimt  1715  equvini  1732  nfexd  1735  ax10oe  1770  sbcof2  1783  spsbim  1816  mor  2042  rexim  2529  elex22  2704  elex2  2705  vtoclegft  2761  spcimgft  2765  spcimegft  2767  spc2gv  2780  spc3gv  2782  ssoprab2  5835  bj-inf2vnlem1  13339