Theorem eximi 1649

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

Hypothesis

Ref	Expression
eximi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
eximi	⊢ (∃𝑥𝜑 → ∃𝑥𝜓)

Proof of Theorem eximi

Step	Hyp	Ref	Expression
1		exim 1648	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		eximi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1500	1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1541

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1650  eximii  1651  exsimpl  1666  exsimpr  1667  19.29r2  1671  19.29x  1672  19.35-1  1673  19.43  1677  19.40  1680  19.40-2  1681  exanaliim  1696  19.12  1713  equs4  1773  cbvexh  1804  equvini  1807  sbimi  1813  equs5e  1844  exdistrfor  1849  equs45f  1851  sbcof2  1859  sbequi  1888  spsbe  1891  sbidm  1900  cbvexdh  1978  eumo0  2113  mor  2125  euan  2139  eupickb  2164  2eu2ex  2172  2exeu  2175  rexex  2590  reximi2  2640  cgsexg  2851  gencbvex  2863  gencbval  2865  vtocl3  2873  eqvinc  2942  eqvincg  2943  mosubt  2996  rexm  3611  prmg  3816  bm1.3ii  4233  a9evsep  4234  axnul  4237  reldmm  4977  elrelimasn  5130  dminss  5179  imainss  5180  euiotaex  5331  imadiflem  5437  funimaexglem  5441  brprcneu  5665  fv3  5695  relelfvdm  5704  ssimaex  5740  oprabid  6084  brabvv  6101  uchoice  6333  ecexr  6774  enssdom  7003  fidcenumlemim  7224  subhalfnqq  7734  prarloc  7823  ltexprlemopl  7921  ltexprlemlol  7922  ltexprlemopu  7923  ltexprlemupu  7924  fnpr2ob  13574  fngsum  13622  igsumvalx  13623  bdbm1.3ii  16710  bj-inex  16726  bj-2inf  16757