Theorem exim 1536

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 1479	. 2 |- ( A. x ( ph -> ps ) -> A. x A. x ( ph -> ps ) )
2		hbe1 1430	. 2 |- ( E. x ps -> A. x E. x ps )
3		19.8a 1528	. . . 4 |- ( ps -> E. x ps )
4	3	imim2i 12	. . 3 |- ( ( ph -> ps ) -> ( ph -> E. x ps ) )
5	4	sps 1476	. 2 |- ( A. x ( ph -> ps ) -> ( ph -> E. x ps ) )
6	1, 2, 5	exlimdh 1533	1 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )

Syntax hints:   -> wi 4   A.wal 1288   E.wex 1427

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-ial 1473

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eximi  1537  exbi  1541  eximdh  1548  19.29  1557  19.25  1563  alexim  1582  19.23t  1613  spimt  1672  equvini  1689  nfexd  1692  ax10oe  1726  sbcof2  1739  spsbim  1772  mor  1991  rexim  2468  elex22  2635  elex2  2636  vtoclegft  2692  spcimgft  2696  spcimegft  2698  spc2gv  2710  spc3gv  2712  ssoprab2  5719  bj-inf2vnlem1  12138