Theorem eximi 1752

Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.)

Hypothesis

Ref	Expression
eximi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
eximi	⊢ (∃𝑥𝜑 → ∃𝑥𝜓)

Proof of Theorem eximi

Step	Hyp	Ref	Expression
1		exim 1751	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		eximi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1715	1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  2eximi  1753  eximii  1754  exa1  1756  exan  1775  exsimpl  1783  exsimpr  1784  19.29r2  1792  19.29x  1793  19.35  1794  19.40-2  1803  exlimiv  1845  speimfwALT  1864  sbimi  1873  19.12  2150  ax13lem2  2284  exdistrf  2321  equs45f  2338  mo2v  2465  2eu2ex  2534  reximi2  2993  cgsexg  3211  gencbvex  3223  vtocl3  3235  eqvinc  3300  axrep2  4701  bm1.3ii  4712  ax6vsep  4713  copsexg  4882  relopabi  5167  dminss  5466  imainss  5467  elsnxpOLD  5595  iotaex  5785  fv3  6116  ssimaex  6173  dffv2  6181  exfo  6285  oprabid  6576  zfrep6  7027  frxp  7174  suppimacnvss  7192  tz7.48-1  7425  enssdom  7866  fineqvlem  8059  infcntss  8119  infeq5  8417  omex  8423  rankuni  8609  scott0  8632  acni3  8753  acnnum  8758  dfac3  8827  dfac9  8841  kmlem1  8855  cflm  8955  cfcof  8979  axdc4lem  9160  axcclem  9162  ac6c4  9186  ac6s  9189  ac6s2  9191  axdclem2  9225  brdom3  9231  brdom5  9232  brdom4  9233  nqpr  9715  ltexprlem4  9740  reclem2pr  9749  hash1to3  13128  trclublem  13582  drsdirfi  16761  2ndcsb  21062  fbssint  21452  isfil2  21470  alexsubALTlem3  21663  lpbl  22118  metustfbas  22172  3v3e3cycl2  26192  ex-natded9.26-2  26669  eqvincg  28698  19.9d2rf  28702  rexunirn  28715  f1ocnt  28946  fmcncfil  29305  esumiun  29483  0elsiga  29504  ddemeas  29626  bnj168  30052  bnj593  30069  bnj607  30240  bnj600  30243  bnj916  30257  fundmpss  30910  exisym1  31593  bj-exlime  31796  bj-nalnaleximiOLD  31798  bj-sbex  31815  bj-ssbequ2  31832  bj-equs45fv  31940  bj-axrep2  31977  bj-eumo0  32018  bj-snsetex  32144  bj-snglss  32151  bj-snglex  32154  bj-restn0  32224  bj-toprntopon  32244  bj-ccinftydisj  32277  mptsnunlem  32361  spsbce-2  37602  iotaexeu  37641  iotasbc  37642  relopabVD  38159  ax6e2ndeqVD  38167  2uasbanhVD  38169  ax6e2ndeqALT  38189  fnchoice  38211  rfcnnnub  38218  stoweidlem35  38928  stoweidlem57  38950  n0rex  40310