Theorem eximi 1648

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

Syntax hints:   → wi 4  ∃wex 1540

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1649  eximii  1650  exsimpl  1665  exsimpr  1666  19.29r2  1670  19.29x  1671  19.35-1  1672  19.43  1676  19.40  1679  19.40-2  1680  exanaliim  1695  19.12  1712  equs4  1772  cbvexh  1802  equvini  1805  sbimi  1811  equs5e  1842  exdistrfor  1847  equs45f  1849  sbcof2  1857  sbequi  1886  spsbe  1889  sbidm  1898  cbvexdh  1974  eumo0  2109  mor  2121  euan  2135  eupickb  2160  2eu2ex  2168  2exeu  2171  rexex  2577  reximi2  2627  cgsexg  2837  gencbvex  2849  gencbval  2851  vtocl3  2859  eqvinc  2928  eqvincg  2929  mosubt  2982  rexm  3593  prmg  3795  bm1.3ii  4211  a9evsep  4212  axnul  4215  reldmm  4952  elrelimasn  5104  dminss  5153  imainss  5154  euiotaex  5305  imadiflem  5411  funimaexglem  5415  brprcneu  5635  fv3  5665  relelfvdm  5674  ssimaex  5710  oprabid  6055  brabvv  6072  uchoice  6305  ecexr  6712  enssdom  6940  fidcenumlemim  7156  subhalfnqq  7639  prarloc  7728  ltexprlemopl  7826  ltexprlemlol  7827  ltexprlemopu  7828  ltexprlemupu  7829  fnpr2ob  13446  fngsum  13494  igsumvalx  13495  bdbm1.3ii  16546  bj-inex  16562  bj-2inf  16593