Theorem eximi 1653

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

Syntax hints:   → wi 4  ∃wex 1545

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1654  eximii  1655  exsimpl  1670  exsimpr  1671  19.29r2  1675  19.29x  1676  19.35-1  1677  19.43  1681  19.40  1684  19.40-2  1685  exanaliim  1700  19.12  1717  equs4  1777  cbvexh  1808  equvini  1811  sbimi  1817  equs5e  1848  exdistrfor  1853  equs45f  1855  sbcof2  1863  sbequi  1892  spsbe  1895  sbidm  1904  cbvexdh  1982  eumo0  2117  mor  2129  euan  2143  eupickb  2168  2eu2ex  2176  2exeu  2179  rexex  2596  reximi2  2646  cgsexg  2857  gencbvex  2869  gencbval  2871  vtocl3  2879  eqvinc  2949  eqvincg  2950  mosubt  3003  rexm  3627  prmg  3833  bm1.3ii  4252  a9evsep  4253  axnul  4256  reldmm  4998  elrelimasn  5151  dminss  5200  imainss  5201  euiotaex  5352  imadiflem  5458  funimaexglem  5462  brprcneu  5686  fv3  5716  relelfvdm  5725  ssimaex  5761  mptmex  5939  oprabid  6111  brabvv  6128  uchoice  6365  ecexr  6806  enssdom  7042  fidcenumlemim  7263  subhalfnqq  7775  prarloc  7864  ltexprlemopl  7962  ltexprlemlol  7963  ltexprlemopu  7964  ltexprlemupu  7965  fnpr2ob  13644  fngzsum  13691  gzsumvalx  13692  bdbm1.3ii  16900  bj-inex  16916  bj-2inf  16947