Theorem eximi 1600

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

Syntax hints:   → wi 4  ∃wex 1492

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1601  eximii  1602  exsimpl  1617  exsimpr  1618  19.29r2  1622  19.29x  1623  19.35-1  1624  19.43  1628  19.40  1631  19.40-2  1632  exanaliim  1647  19.12  1665  equs4  1725  cbvexh  1755  equvini  1758  sbimi  1764  equs5e  1795  exdistrfor  1800  equs45f  1802  sbcof2  1810  sbequi  1839  spsbe  1842  sbidm  1851  cbvexdh  1926  eumo0  2057  mor  2068  euan  2082  eupickb  2107  2eu2ex  2115  2exeu  2118  rexex  2523  reximi2  2573  cgsexg  2773  gencbvex  2784  gencbval  2786  vtocl3  2794  eqvinc  2861  eqvincg  2862  mosubt  2915  rexm  3523  prmg  3714  bm1.3ii  4125  a9evsep  4126  axnul  4129  elrelimasn  4995  dminss  5044  imainss  5045  euiotaex  5195  imadiflem  5296  funimaexglem  5300  brprcneu  5509  fv3  5539  relelfvdm  5548  ssimaex  5578  oprabid  5907  brabvv  5921  ecexr  6540  enssdom  6762  fidcenumlemim  6951  subhalfnqq  7413  prarloc  7502  ltexprlemopl  7600  ltexprlemlol  7601  ltexprlemopu  7602  ltexprlemupu  7603  fnpr2ob  12759  bdbm1.3ii  14646  bj-inex  14662  bj-2inf  14693