Theorem eximi 1646

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

Syntax hints:   → wi 4  ∃wex 1538

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1647  eximii  1648  exsimpl  1663  exsimpr  1664  19.29r2  1668  19.29x  1669  19.35-1  1670  19.43  1674  19.40  1677  19.40-2  1678  exanaliim  1693  19.12  1711  equs4  1771  cbvexh  1801  equvini  1804  sbimi  1810  equs5e  1841  exdistrfor  1846  equs45f  1848  sbcof2  1856  sbequi  1885  spsbe  1888  sbidm  1897  cbvexdh  1973  eumo0  2108  mor  2120  euan  2134  eupickb  2159  2eu2ex  2167  2exeu  2170  rexex  2576  reximi2  2626  cgsexg  2835  gencbvex  2847  gencbval  2849  vtocl3  2857  eqvinc  2926  eqvincg  2927  mosubt  2980  rexm  3591  prmg  3789  bm1.3ii  4205  a9evsep  4206  axnul  4209  reldmm  4942  elrelimasn  5094  dminss  5143  imainss  5144  euiotaex  5295  imadiflem  5400  funimaexglem  5404  brprcneu  5622  fv3  5652  relelfvdm  5661  ssimaex  5697  oprabid  6039  brabvv  6056  uchoice  6289  ecexr  6693  enssdom  6921  fidcenumlemim  7127  subhalfnqq  7609  prarloc  7698  ltexprlemopl  7796  ltexprlemlol  7797  ltexprlemopu  7798  ltexprlemupu  7799  fnpr2ob  13381  fngsum  13429  igsumvalx  13430  bdbm1.3ii  16278  bj-inex  16294  bj-2inf  16325