Theorem eximi 1532

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 1531	. 2 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
2		eximi.1	. 2 |- ( ph -> ps )
3	1, 2	mpg 1381	1 |- ( E. x ph -> E. x ps )

Syntax hints:   -> wi 4   E.wex 1422

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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-ial 1468

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  2eximi  1533  eximii  1534  exsimpl  1549  exsimpr  1550  19.29r2  1554  19.29x  1555  19.35-1  1556  19.43  1560  19.40  1563  19.40-2  1564  exanaliim  1579  19.12  1596  equs4  1654  cbvexh  1679  equvini  1682  sbimi  1688  equs5e  1717  exdistrfor  1722  equs45f  1724  sbcof2  1732  sbequi  1761  spsbe  1764  sbidm  1773  cbvexdh  1843  eumo0  1973  mor  1984  euan  1998  eupickb  2023  2eu2ex  2031  2exeu  2034  rexex  2411  reximi2  2458  cgsexg  2635  gencbvex  2646  gencbval  2648  vtocl3  2656  eqvinc  2719  eqvincg  2720  mosubt  2770  rexm  3348  prmg  3519  bm1.3ii  3907  a9evsep  3908  axnul  3911  dminss  4768  imainss  4769  euiotaex  4913  imadiflem  5009  funimaexglem  5013  brprcneu  5202  fv3  5229  relelfvdm  5237  ssimaex  5266  oprabid  5568  brabvv  5582  ecexr  6177  enssdom  6309  subhalfnqq  6666  prarloc  6755  ltexprlemopl  6853  ltexprlemlol  6854  ltexprlemopu  6855  ltexprlemupu  6856  bdbm1.3ii  10840  bj-inex  10856  bj-2inf  10891