Theorem eximi 1865

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

Syntax hints:   → wi 4  ∃wex 1809

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

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  2eximi  1866  eximii  1867  exa1  1868  exsimpl  1898  exsimpr  1899  19.29r2  1905  19.29x  1906  19.35  1907  19.40-2  1917  emptyex  1937  exlimiv  1960  speimfwALT  1994  nfexhe  2211  19.12  2360  ax13lem2  2408  exdistrf  2479  equs45f  2491  dfmoeu  2563  eu6  2602  2eu2ex  2671  reximi2  3098  cgsexg  3499  gencbvex  3511  eqvincg  3608  sbcg  3817  n0rex  4313  axrep2  5242  sepex  5264  bm1.3iiOLD  5266  ax6vsep  5267  axprg  5410  copsexgwOLD  5475  copsexg  5476  relopabi  5811  dmcoss  5967  dminss  6152  imainss  6153  iotanul2  6511  fv3  6901  ssimaex  6968  dffv2  6978  exfo  7102  oprabidw  7443  oprabid  7444  zfrep6OLD  7953  frxp  8123  suppimacnvss  8170  tz7.48-1  8431  enssdom  8974  enssdomOLD  8975  enfii  9171  fineqvlem  9227  enp1i  9240  infcntss  9283  infeq5  9607  rankuni  9836  scott0  9861  acni3  10032  acnnum  10037  dfac3  10106  dfac9  10121  kmlem1  10135  cflm  10234  cfcof  10259  axdc4lem  10440  axcclem  10442  ac6c4  10466  ac6s  10469  ac6s2  10471  axdclem2  10505  brdom3  10513  brdom5  10514  brdom4  10515  nqpr  11000  ltexprlem4  11025  reclem2pr  11034  hash1to3  14531  trclublem  15034  fnpr2ob  17613  drsdirfi  18362  toprntopon  23063  2ndcsb  23587  fbssint  23976  isfil2  23994  alexsubALTlem3  24187  lpbl  24641  metustfbas  24695  lrrecfr  28114  ex-natded9.26-2  30749  19.9d2rf  32794  rexunirn  32816  f1ocnt  33123  fsumiunle  33151  fmcncfil  34299  esumiun  34462  0elsiga  34482  ddemeas  34604  bnj168  35097  bnj593  35112  bnj607  35282  bnj600  35285  bnj916  35299  axprALT2  35481  fineqvpow  35506  tz9.1regs  35525  kardeq0  35547  onvf1odlem1  35565  wevgblacfn  35573  lfuhgr3  35590  cusgredgex  35592  loop1cycl  35607  umgr2cycl  35611  fundmpss  36237  exisym1  36913  axtco2g  36966  bj-sylge  37207  bj-exextruan  37238  bj-cbvew  37242  bj-19.12  37326  bj-equs45fv  37424  bj-snsetex  37577  bj-snglss  37584  bj-snglex  37587  bj-bm1.3ii  37678  bj-axnul  37687  bj-axseprep  37689  bj-restn0  37710  bj-ccinftydisj  37835  mptsnunlem  37962  pibt2  38041  wl-cbvmotv  38146  wl-moae  38149  wl-nax6im  38151  eu6w  43388  iscard4  44239  ismnushort  44991  spsbce-2  45071  iotaexeu  45108  iotasbc  45109  relopabVD  45589  ax6e2ndeqVD  45597  2uasbanhVD  45599  ax6e2ndeqALT  45619  fnchoice  45729  rfcnnnub  45736  stoweidlem35  46729  stoweidlem57  46751  mo0sn  49571