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  3483  gencbvex  3498  eqvincg  3605  sbcg  3817  n0rex  4310  axrep2  5224  sepex  5242  bm1.3iiOLD  5244  ax6vsep  5245  copsexgw  5437  copsexg  5438  relopabi  5769  dmcoss  5920  dminss  6106  imainss  6107  iotanul2  6459  fv3  6844  ssimaex  6912  dffv2  6922  exfo  7043  oprabidw  7384  oprabid  7385  zfrep6  7897  frxp  8066  suppimacnvss  8113  tz7.48-1  8372  enssdom  8909  enfii  9110  fineqvlem  9167  enp1i  9182  infcntss  9231  infeq5  9552  rankuni  9778  scott0  9801  acni3  9960  acnnum  9965  dfac3  10034  dfac9  10050  kmlem1  10064  cflm  10163  cfcof  10187  axdc4lem  10368  axcclem  10370  ac6c4  10394  ac6s  10397  ac6s2  10399  axdclem2  10433  brdom3  10441  brdom5  10442  brdom4  10443  nqpr  10927  ltexprlem4  10952  reclem2pr  10961  hash1to3  14417  trclublem  14920  fnpr2ob  17480  drsdirfi  18229  toprntopon  22828  2ndcsb  23352  fbssint  23741  isfil2  23759  alexsubALTlem3  23952  lpbl  24407  metustfbas  24461  lrrecfr  27873  ex-natded9.26-2  30382  19.9d2rf  32431  rexunirn  32454  f1ocnt  32758  fsumiunle  32787  fmcncfil  33897  esumiun  34060  0elsiga  34080  ddemeas  34202  bnj168  34696  bnj593  34711  bnj607  34882  bnj600  34885  bnj916  34899  tz9.1regs  35066  fineqvpow  35070  onvf1odlem1  35075  wevgblacfn  35081  lfuhgr3  35092  cusgredgex  35094  loop1cycl  35109  umgr2cycl  35113  fundmpss  35739  exisym1  36397  bj-sylge  36597  bj-19.12  36734  bj-equs45fv  36784  bj-snsetex  36936  bj-snglss  36943  bj-snglex  36946  bj-bm1.3ii  37037  bj-restn0  37063  bj-ccinftydisj  37186  mptsnunlem  37311  pibt2  37390  wl-cbvmotv  37486  wl-moae  37489  wl-nax6im  37491  eu6w  42649  iscard4  43506  ismnushort  44274  spsbce-2  44354  iotaexeu  44391  iotasbc  44392  relopabVD  44874  ax6e2ndeqVD  44882  2uasbanhVD  44884  ax6e2ndeqALT  44904  fnchoice  45007  rfcnnnub  45014  stoweidlem35  46017  stoweidlem57  46039  mo0sn  48801