Theorem eximi 1491

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

Syntax hints:   → wi 4  ∃wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-ial 1427

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2eximi  1492  eximii  1493  exsimpl  1508  exsimpr  1509  19.29r2  1513  19.29x  1514  19.35-1  1515  19.43  1519  19.40  1522  19.40-2  1523  exanaliim  1538  19.12  1555  equs4  1613  cbvexh  1638  equvini  1641  sbimi  1647  equs5e  1676  exdistrfor  1681  equs45f  1683  sbcof2  1691  sbequi  1720  spsbe  1723  sbidm  1731  cbvexdh  1801  eumo0  1931  mor  1942  euan  1956  eupickb  1981  2eu2ex  1989  2exeu  1992  rexex  2368  reximi2  2415  cgsexg  2589  gencbvex  2600  gencbval  2602  vtocl3  2610  eqvinc  2667  eqvincg  2668  mosubt  2718  rexm  3320  prmg  3489  bm1.3ii  3878  a9evsep  3879  axnul  3882  dtruex  4283  dminss  4738  imainss  4739  euiotaex  4883  imadiflem  4978  funimaexglem  4982  brprcneu  5171  fv3  5197  relelfvdm  5205  ssimaex  5234  oprabid  5537  brabvv  5551  ecexr  6111  enssdom  6242  subhalfnqq  6512  prarloc  6601  ltexprlemopl  6699  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  bdbm1.3ii  10011  bj-inex  10027  bj-2inf  10062