Theorem exim 1490

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 1433	. 2 |- ( A. x ( ph -> ps ) -> A. x A. x ( ph -> ps ) )
2		hbe1 1384	. 2 |- ( E. x ps -> A. x E. x ps )
3		19.8a 1482	. . . 4 |- ( ps -> E. x ps )
4	3	imim2i 12	. . 3 |- ( ( ph -> ps ) -> ( ph -> E. x ps ) )
5	4	sps 1430	. 2 |- ( A. x ( ph -> ps ) -> ( ph -> E. x ps ) )
6	1, 2, 5	exlimdh 1487	1 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )

Syntax hints:   -> wi 4   A.wal 1241   E.wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-ial 1427

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  eximi  1491  exbi  1495  eximdh  1502  19.29  1511  19.25  1517  alexim  1536  19.23t  1567  spimt  1624  equvini  1641  nfexd  1644  ax10oe  1678  sbcof2  1691  spsbim  1724  mor  1942  rexim  2413  elex22  2569  elex2  2570  vtoclegft  2625  spcimgft  2629  spcimegft  2631  spc2gv  2643  spc3gv  2645  ssoprab2  5561  bj-inf2vnlem1  10095