Theorem eximi 1579

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

Syntax hints:   → wi 4  ∃wex 1468

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximi  1580  eximii  1581  exsimpl  1596  exsimpr  1597  19.29r2  1601  19.29x  1602  19.35-1  1603  19.43  1607  19.40  1610  19.40-2  1611  exanaliim  1626  19.12  1643  equs4  1703  cbvexh  1728  equvini  1731  sbimi  1737  equs5e  1767  exdistrfor  1772  equs45f  1774  sbcof2  1782  sbequi  1811  spsbe  1814  sbidm  1823  cbvexdh  1898  eumo0  2030  mor  2041  euan  2055  eupickb  2080  2eu2ex  2088  2exeu  2091  rexex  2479  reximi2  2528  cgsexg  2721  gencbvex  2732  gencbval  2734  vtocl3  2742  eqvinc  2808  eqvincg  2809  mosubt  2861  rexm  3462  prmg  3644  bm1.3ii  4049  a9evsep  4050  axnul  4053  dminss  4953  imainss  4954  euiotaex  5104  imadiflem  5202  funimaexglem  5206  brprcneu  5414  fv3  5444  relelfvdm  5453  ssimaex  5482  oprabid  5803  brabvv  5817  ecexr  6434  enssdom  6656  fidcenumlemim  6840  subhalfnqq  7222  prarloc  7311  ltexprlemopl  7409  ltexprlemlol  7410  ltexprlemopu  7411  ltexprlemupu  7412  bdbm1.3ii  13089  bj-inex  13105  bj-2inf  13136