Theorem eximi 1624

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

Syntax hints:   → wi 4  ∃wex 1516

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1625  eximii  1626  exsimpl  1641  exsimpr  1642  19.29r2  1646  19.29x  1647  19.35-1  1648  19.43  1652  19.40  1655  19.40-2  1656  exanaliim  1671  19.12  1689  equs4  1749  cbvexh  1779  equvini  1782  sbimi  1788  equs5e  1819  exdistrfor  1824  equs45f  1826  sbcof2  1834  sbequi  1863  spsbe  1866  sbidm  1875  cbvexdh  1951  eumo0  2086  mor  2097  euan  2111  eupickb  2136  2eu2ex  2144  2exeu  2147  rexex  2553  reximi2  2603  cgsexg  2808  gencbvex  2820  gencbval  2822  vtocl3  2830  eqvinc  2897  eqvincg  2898  mosubt  2951  rexm  3561  prmg  3756  bm1.3ii  4169  a9evsep  4170  axnul  4173  elrelimasn  5053  dminss  5102  imainss  5103  euiotaex  5253  imadiflem  5358  funimaexglem  5362  brprcneu  5576  fv3  5606  relelfvdm  5615  ssimaex  5647  oprabid  5983  brabvv  5998  uchoice  6230  ecexr  6632  enssdom  6860  fidcenumlemim  7061  subhalfnqq  7534  prarloc  7623  ltexprlemopl  7721  ltexprlemlol  7722  ltexprlemopu  7723  ltexprlemupu  7724  fnpr2ob  13216  fngsum  13264  igsumvalx  13265  bdbm1.3ii  15901  bj-inex  15917  bj-2inf  15948