Theorem eximi 1580

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 1579	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		eximi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1428	1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-ial 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximi  1581  eximii  1582  exsimpl  1597  exsimpr  1598  19.29r2  1602  19.29x  1603  19.35-1  1604  19.43  1608  19.40  1611  19.40-2  1612  exanaliim  1627  19.12  1644  equs4  1704  cbvexh  1729  equvini  1732  sbimi  1738  equs5e  1768  exdistrfor  1773  equs45f  1775  sbcof2  1783  sbequi  1812  spsbe  1815  sbidm  1824  cbvexdh  1899  eumo0  2031  mor  2042  euan  2056  eupickb  2081  2eu2ex  2089  2exeu  2092  rexex  2482  reximi2  2531  cgsexg  2724  gencbvex  2735  gencbval  2737  vtocl3  2745  eqvinc  2812  eqvincg  2813  mosubt  2865  rexm  3467  prmg  3652  bm1.3ii  4057  a9evsep  4058  axnul  4061  dminss  4961  imainss  4962  euiotaex  5112  imadiflem  5210  funimaexglem  5214  brprcneu  5422  fv3  5452  relelfvdm  5461  ssimaex  5490  oprabid  5811  brabvv  5825  ecexr  6442  enssdom  6664  fidcenumlemim  6848  subhalfnqq  7246  prarloc  7335  ltexprlemopl  7433  ltexprlemlol  7434  ltexprlemopu  7435  ltexprlemupu  7436  bdbm1.3ii  13260  bj-inex  13276  bj-2inf  13307