Theorem eximi 1649

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

Syntax hints:   → wi 4  ∃wex 1541

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1650  eximii  1651  exsimpl  1666  exsimpr  1667  19.29r2  1671  19.29x  1672  19.35-1  1673  19.43  1677  19.40  1680  19.40-2  1681  exanaliim  1696  19.12  1713  equs4  1773  cbvexh  1804  equvini  1807  sbimi  1813  equs5e  1844  exdistrfor  1849  equs45f  1851  sbcof2  1859  sbequi  1888  spsbe  1891  sbidm  1900  cbvexdh  1976  eumo0  2111  mor  2123  euan  2137  eupickb  2162  2eu2ex  2170  2exeu  2173  rexex  2588  reximi2  2638  cgsexg  2848  gencbvex  2860  gencbval  2862  vtocl3  2870  eqvinc  2939  eqvincg  2940  mosubt  2993  rexm  3608  prmg  3813  bm1.3ii  4230  a9evsep  4231  axnul  4234  reldmm  4974  elrelimasn  5127  dminss  5176  imainss  5177  euiotaex  5328  imadiflem  5434  funimaexglem  5438  brprcneu  5662  fv3  5692  relelfvdm  5701  ssimaex  5737  oprabid  6081  brabvv  6098  uchoice  6330  ecexr  6771  enssdom  7000  fidcenumlemim  7221  subhalfnqq  7725  prarloc  7814  ltexprlemopl  7912  ltexprlemlol  7913  ltexprlemopu  7914  ltexprlemupu  7915  fnpr2ob  13542  fngsum  13590  igsumvalx  13591  bdbm1.3ii  16648  bj-inex  16664  bj-2inf  16695