Theorem eximi 1600

Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eximi.1	|- ( ph -> ps )

Assertion

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

Proof of Theorem eximi

Step	Hyp	Ref	Expression
1		exim 1599	. 2 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
2		eximi.1	. 2 |- ( ph -> ps )
3	1, 2	mpg 1451	1 |- ( E. x ph -> E. x ps )

Syntax hints:   -> wi 4   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1601  eximii  1602  exsimpl  1617  exsimpr  1618  19.29r2  1622  19.29x  1623  19.35-1  1624  19.43  1628  19.40  1631  19.40-2  1632  exanaliim  1647  19.12  1665  equs4  1725  cbvexh  1755  equvini  1758  sbimi  1764  equs5e  1795  exdistrfor  1800  equs45f  1802  sbcof2  1810  sbequi  1839  spsbe  1842  sbidm  1851  cbvexdh  1926  eumo0  2057  mor  2068  euan  2082  eupickb  2107  2eu2ex  2115  2exeu  2118  rexex  2523  reximi2  2573  cgsexg  2772  gencbvex  2783  gencbval  2785  vtocl3  2793  eqvinc  2860  eqvincg  2861  mosubt  2914  rexm  3522  prmg  3713  bm1.3ii  4124  a9evsep  4125  axnul  4128  elrelimasn  4994  dminss  5043  imainss  5044  euiotaex  5194  imadiflem  5295  funimaexglem  5299  brprcneu  5508  fv3  5538  relelfvdm  5547  ssimaex  5577  oprabid  5906  brabvv  5920  ecexr  6539  enssdom  6761  fidcenumlemim  6950  subhalfnqq  7412  prarloc  7501  ltexprlemopl  7599  ltexprlemlol  7600  ltexprlemopu  7601  ltexprlemupu  7602  fnpr2ob  12758  bdbm1.3ii  14613  bj-inex  14629  bj-2inf  14660