Theorem eximi 1867

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  2eximi  1868  eximii  1869  exa1  1870  exsimpl  1900  exsimpr  1901  19.29r2  1907  19.29x  1908  19.35  1909  19.40-2  1919  emptyex  1939  exlimiv  1962  speimfwALT  1996  nfexhe  2210  ax12ev2c  2216  19.12  2357  ax13lem2  2405  exdistrf  2476  equs45f  2488  dfmoeu  2560  eu6  2599  2eu2ex  2668  reximi2  3095  cgsexg  3494  gencbvex  3506  eqvincg  3601  sbcg  3810  n0rex  4304  axrep2  5234  sepex  5254  ax6vsep  5256  axprg  5394  copsexgwOLD  5460  copsexg  5461  relopabi  5799  dmcoss  5956  dminss  6142  imainss  6143  iotanul2  6511  fv3  6903  ssimaex  6970  dffv2  6980  exfo  7105  oprabidw  7451  oprabid  7452  zfrep6OLD  7967  frxp  8140  suppimacnvss  8193  tz7.48-1  8456  enssdom  9006  enssdomOLD  9007  enfii  9204  fineqvlem  9260  enp1i  9273  infcntss  9317  infeq5  9641  rankuni  9882  scott0b  9940  scott0OLD  9941  acni3  10129  acnnum  10134  dfac3  10203  dfac9  10218  kmlem1  10232  cflm  10330  cfcof  10355  axdc4lem  10536  axcclem  10538  ac6c4  10562  ac6s  10565  ac6s2  10567  axdclem2  10601  brdom3  10610  brdom5  10611  brdom4  10612  nqpr  11102  ltexprlem4  11127  reclem2pr  11136  hash1to3  14640  trclublem  15153  fnpr2ob  17735  drsdirfi  18484  toprntopon  23248  2ndcsb  23772  fbssint  24162  isfil2  24180  alexsubALTlem3  24373  lpbl  24827  metustfbas  24881  lrrecfr  28334  lfuhgr3  29733  loop1cycl  30749  umgr2cycl  30752  ex-natded9.26-2  31026  19.9d2rf  33113  rexunirn  33135  f1ocnt  33438  fsumiunle  33466  fmcncfil  34609  esumiun  34772  0elsiga  34792  ddemeas  34915  bnj168  35407  bnj593  35422  bnj607  35592  bnj600  35595  bnj916  35609  abweex  35769  axprALT2  35786  acwer1prclem  35815  fineqvpow  35839  tz9.1regs  35858  kardeq0  35880  onvf1odlem1  35950  wevgblacfn  35958  cusgredgex  35982  ptpconn  36084  fundmpss  36624  exisym1  37304  axtco2g  37357  bj-sylge  37598  bj-exextruan  37629  bj-cbvew  37633  bj-19.12  37717  bj-equs45fv  37815  bj-snsetex  37968  bj-snglss  37975  bj-snglex  37978  bj-bm1.3ii  38071  bj-axnul  38080  bj-axseprep  38082  bj-restn0  38103  bj-ccinftydisj  38227  mptsnunlem  38354  pibt2  38433  wl-cbvmotv  38538  wl-moae  38541  wl-nax6im  38543  impprop  38737  eu6w  43780  iscard4  44627  ismnushort  45378  spsbce-2  45458  iotaexeu  45495  iotasbc  45496  relopabVD  45976  ax6e2ndeqVD  45984  2uasbanhVD  45986  ax6e2ndeqALT  46006  fnchoice  46139  rfcnnnub  46146  stoweidlem35  47138  stoweidlem57  47160  mo0sn  50020