Theorem eximi 1580

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

Syntax hints:   → wi 4  ∃wex 1472

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximi  1581  eximii  1582  exsimpl  1597  exsimpr  1598  19.29r2  1602  19.29x  1603  19.35-1  1604  19.43  1608  19.40  1611  19.40-2  1612  exanaliim  1627  19.12  1645  equs4  1705  cbvexh  1735  equvini  1738  sbimi  1744  equs5e  1775  exdistrfor  1780  equs45f  1782  sbcof2  1790  sbequi  1819  spsbe  1822  sbidm  1831  cbvexdh  1906  eumo0  2037  mor  2048  euan  2062  eupickb  2087  2eu2ex  2095  2exeu  2098  rexex  2503  reximi2  2553  cgsexg  2747  gencbvex  2758  gencbval  2760  vtocl3  2768  eqvinc  2835  eqvincg  2836  mosubt  2889  rexm  3493  prmg  3680  bm1.3ii  4085  a9evsep  4086  axnul  4089  dminss  4999  imainss  5000  euiotaex  5150  imadiflem  5248  funimaexglem  5252  brprcneu  5460  fv3  5490  relelfvdm  5499  ssimaex  5528  oprabid  5850  brabvv  5864  ecexr  6482  enssdom  6704  fidcenumlemim  6893  subhalfnqq  7328  prarloc  7417  ltexprlemopl  7515  ltexprlemlol  7516  ltexprlemopu  7517  ltexprlemupu  7518  bdbm1.3ii  13437  bj-inex  13453  bj-2inf  13484