Theorem eximi 1611

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

Syntax hints:   → wi 4  ∃wex 1503

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1612  eximii  1613  exsimpl  1628  exsimpr  1629  19.29r2  1633  19.29x  1634  19.35-1  1635  19.43  1639  19.40  1642  19.40-2  1643  exanaliim  1658  19.12  1676  equs4  1736  cbvexh  1766  equvini  1769  sbimi  1775  equs5e  1806  exdistrfor  1811  equs45f  1813  sbcof2  1821  sbequi  1850  spsbe  1853  sbidm  1862  cbvexdh  1938  eumo0  2073  mor  2084  euan  2098  eupickb  2123  2eu2ex  2131  2exeu  2134  rexex  2540  reximi2  2590  cgsexg  2795  gencbvex  2807  gencbval  2809  vtocl3  2817  eqvinc  2884  eqvincg  2885  mosubt  2938  rexm  3547  prmg  3740  bm1.3ii  4151  a9evsep  4152  axnul  4155  elrelimasn  5032  dminss  5081  imainss  5082  euiotaex  5232  imadiflem  5334  funimaexglem  5338  brprcneu  5548  fv3  5578  relelfvdm  5587  ssimaex  5619  oprabid  5951  brabvv  5965  uchoice  6192  ecexr  6594  enssdom  6818  fidcenumlemim  7013  subhalfnqq  7476  prarloc  7565  ltexprlemopl  7663  ltexprlemlol  7664  ltexprlemopu  7665  ltexprlemupu  7666  fnpr2ob  12926  fngsum  12974  igsumvalx  12975  bdbm1.3ii  15453  bj-inex  15469  bj-2inf  15500