Theorem eximi 1626

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

Syntax hints:   → wi 4  ∃wex 1518

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 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-4 1536  ax-ial 1560

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1627  eximii  1628  exsimpl  1643  exsimpr  1644  19.29r2  1648  19.29x  1649  19.35-1  1650  19.43  1654  19.40  1657  19.40-2  1658  exanaliim  1673  19.12  1691  equs4  1751  cbvexh  1781  equvini  1784  sbimi  1790  equs5e  1821  exdistrfor  1826  equs45f  1828  sbcof2  1836  sbequi  1865  spsbe  1868  sbidm  1877  cbvexdh  1953  eumo0  2088  mor  2100  euan  2114  eupickb  2139  2eu2ex  2147  2exeu  2150  rexex  2556  reximi2  2606  cgsexg  2815  gencbvex  2827  gencbval  2829  vtocl3  2837  eqvinc  2906  eqvincg  2907  mosubt  2960  rexm  3571  prmg  3768  bm1.3ii  4184  a9evsep  4185  axnul  4188  elrelimasn  5070  dminss  5119  imainss  5120  euiotaex  5271  imadiflem  5376  funimaexglem  5380  brprcneu  5596  fv3  5626  relelfvdm  5635  ssimaex  5668  oprabid  6006  brabvv  6021  uchoice  6253  ecexr  6655  enssdom  6883  fidcenumlemim  7087  subhalfnqq  7569  prarloc  7658  ltexprlemopl  7756  ltexprlemlol  7757  ltexprlemopu  7758  ltexprlemupu  7759  fnpr2ob  13339  fngsum  13387  igsumvalx  13388  bdbm1.3ii  16164  bj-inex  16180  bj-2inf  16211