Theorem eximi 1588

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

Syntax hints:   → wi 4  ∃wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximi  1589  eximii  1590  exsimpl  1605  exsimpr  1606  19.29r2  1610  19.29x  1611  19.35-1  1612  19.43  1616  19.40  1619  19.40-2  1620  exanaliim  1635  19.12  1653  equs4  1713  cbvexh  1743  equvini  1746  sbimi  1752  equs5e  1783  exdistrfor  1788  equs45f  1790  sbcof2  1798  sbequi  1827  spsbe  1830  sbidm  1839  cbvexdh  1914  eumo0  2045  mor  2056  euan  2070  eupickb  2095  2eu2ex  2103  2exeu  2106  rexex  2512  reximi2  2562  cgsexg  2761  gencbvex  2772  gencbval  2774  vtocl3  2782  eqvinc  2849  eqvincg  2850  mosubt  2903  rexm  3508  prmg  3697  bm1.3ii  4103  a9evsep  4104  axnul  4107  dminss  5018  imainss  5019  euiotaex  5169  imadiflem  5267  funimaexglem  5271  brprcneu  5479  fv3  5509  relelfvdm  5518  ssimaex  5547  oprabid  5874  brabvv  5888  ecexr  6506  enssdom  6728  fidcenumlemim  6917  subhalfnqq  7355  prarloc  7444  ltexprlemopl  7542  ltexprlemlol  7543  ltexprlemopu  7544  ltexprlemupu  7545  bdbm1.3ii  13773  bj-inex  13789  bj-2inf  13820