Theorem eximi 1614

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

Syntax hints:   → wi 4  ∃wex 1506

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1615  eximii  1616  exsimpl  1631  exsimpr  1632  19.29r2  1636  19.29x  1637  19.35-1  1638  19.43  1642  19.40  1645  19.40-2  1646  exanaliim  1661  19.12  1679  equs4  1739  cbvexh  1769  equvini  1772  sbimi  1778  equs5e  1809  exdistrfor  1814  equs45f  1816  sbcof2  1824  sbequi  1853  spsbe  1856  sbidm  1865  cbvexdh  1941  eumo0  2076  mor  2087  euan  2101  eupickb  2126  2eu2ex  2134  2exeu  2137  rexex  2543  reximi2  2593  cgsexg  2798  gencbvex  2810  gencbval  2812  vtocl3  2820  eqvinc  2887  eqvincg  2888  mosubt  2941  rexm  3551  prmg  3744  bm1.3ii  4155  a9evsep  4156  axnul  4159  elrelimasn  5036  dminss  5085  imainss  5086  euiotaex  5236  imadiflem  5338  funimaexglem  5342  brprcneu  5554  fv3  5584  relelfvdm  5593  ssimaex  5625  oprabid  5957  brabvv  5972  uchoice  6204  ecexr  6606  enssdom  6830  fidcenumlemim  7027  subhalfnqq  7498  prarloc  7587  ltexprlemopl  7685  ltexprlemlol  7686  ltexprlemopu  7687  ltexprlemupu  7688  fnpr2ob  13042  fngsum  13090  igsumvalx  13091  bdbm1.3ii  15621  bj-inex  15637  bj-2inf  15668