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  4945  elrelimasn  5097  dminss  5146  imainss  5147  euiotaex  5298  imadiflem  5403  funimaexglem  5407  brprcneu  5625  fv3  5655  relelfvdm  5664  ssimaex  5700  oprabid  6042  brabvv  6059  uchoice  6292  ecexr  6698  enssdom  6926  fidcenumlemim  7135  subhalfnqq  7617  prarloc  7706  ltexprlemopl  7804  ltexprlemlol  7805  ltexprlemopu  7806  ltexprlemupu  7807  fnpr2ob  13394  fngsum  13442  igsumvalx  13443  bdbm1.3ii  16363  bj-inex  16379  bj-2inf  16410