Theorem eximi 1835

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

Syntax hints:   → wi 4  ∃wex 1779

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

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  2eximi  1836  eximii  1837  exa1  1838  exsimpl  1868  exsimpr  1869  19.29r2  1875  19.29x  1876  19.35  1877  19.40-2  1887  emptyex  1907  exlimiv  1930  speimfwALT  1964  19.12  2326  ax13lem2  2374  exdistrf  2445  equs45f  2457  dfmoeu  2529  moimi  2538  eu6  2567  2eu2ex  2636  reximi2  3062  cgsexg  3492  gencbvex  3507  eqvincg  3614  sbcg  3826  n0rex  4320  axrep2  5237  sepex  5255  bm1.3iiOLD  5257  ax6vsep  5258  copsexgw  5450  copsexg  5451  relopabi  5785  dminss  6126  imainss  6127  iotanul2  6481  iotaexOLD  6491  fv3  6876  ssimaex  6946  dffv2  6956  exfo  7077  oprabidw  7418  oprabid  7419  zfrep6  7933  frxp  8105  suppimacnvss  8152  tz7.48-1  8411  enssdom  8948  enfii  9150  fineqvlem  9209  enp1i  9224  infcntss  9273  infeq5  9590  rankuni  9816  scott0  9839  acni3  10000  acnnum  10005  dfac3  10074  dfac9  10090  kmlem1  10104  cflm  10203  cfcof  10227  axdc4lem  10408  axcclem  10410  ac6c4  10434  ac6s  10437  ac6s2  10439  axdclem2  10473  brdom3  10481  brdom5  10482  brdom4  10483  nqpr  10967  ltexprlem4  10992  reclem2pr  11001  hash1to3  14457  trclublem  14961  fnpr2ob  17521  drsdirfi  18266  toprntopon  22812  2ndcsb  23336  fbssint  23725  isfil2  23743  alexsubALTlem3  23936  lpbl  24391  metustfbas  24445  lrrecfr  27850  ex-natded9.26-2  30349  19.9d2rf  32398  rexunirn  32421  f1ocnt  32725  fsumiunle  32754  fmcncfil  33921  esumiun  34084  0elsiga  34104  ddemeas  34226  bnj168  34720  bnj593  34735  bnj607  34906  bnj600  34909  bnj916  34923  fineqvpow  35086  onvf1odlem1  35090  wevgblacfn  35096  lfuhgr3  35107  cusgredgex  35109  loop1cycl  35124  umgr2cycl  35128  fundmpss  35754  exisym1  36412  bj-sylge  36612  bj-19.12  36749  bj-equs45fv  36799  bj-snsetex  36951  bj-snglss  36958  bj-snglex  36961  bj-bm1.3ii  37052  bj-restn0  37078  bj-ccinftydisj  37201  mptsnunlem  37326  pibt2  37405  wl-cbvmotv  37501  wl-moae  37504  wl-nax6im  37506  eu6w  42664  iscard4  43522  ismnushort  44290  spsbce-2  44370  iotaexeu  44407  iotasbc  44408  relopabVD  44890  ax6e2ndeqVD  44898  2uasbanhVD  44900  ax6e2ndeqALT  44920  fnchoice  45023  rfcnnnub  45030  stoweidlem35  46033  stoweidlem57  46055  mo0sn  48804