Theorem eximi 1858

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

Syntax hints:   → wi 4  ∃wex 1802

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

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

This theorem is referenced by:  2eximi  1859  eximii  1860  exa1  1861  exsimpl  1891  exsimpr  1892  19.29r2  1898  19.29x  1899  19.35  1900  19.40-2  1910  emptyex  1930  exlimiv  1953  speimfwALT  1987  nfexhe  2213  19.12  2362  ax13lem2  2410  exdistrf  2481  equs45f  2493  dfmoeu  2565  eu6  2604  2eu2ex  2673  reximi2  3098  cgsexg  3501  gencbvex  3513  eqvincg  3610  sbcg  3819  n0rex  4313  axrep2  5235  sepex  5255  bm1.3iiOLD  5257  ax6vsep  5258  axprg  5399  copsexgwOLD  5464  copsexg  5465  relopabi  5800  dmcoss  5956  dminss  6142  imainss  6143  iotanul2  6498  fv3  6889  ssimaex  6956  dffv2  6966  exfo  7090  oprabidw  7431  oprabid  7432  zfrep6OLD  7940  frxp  8110  suppimacnvss  8157  tz7.48-1  8418  enssdom  8961  enssdomOLD  8962  enfii  9158  fineqvlem  9214  enp1i  9227  infcntss  9270  infeq5  9594  rankuni  9823  scott0  9848  acni3  10019  acnnum  10024  dfac3  10093  dfac9  10108  kmlem1  10122  cflm  10221  cfcof  10246  axdc4lem  10427  axcclem  10429  ac6c4  10453  ac6s  10456  ac6s2  10458  axdclem2  10492  brdom3  10500  brdom5  10501  brdom4  10502  nqpr  10987  ltexprlem4  11012  reclem2pr  11021  hash1to3  14519  trclublem  15022  fnpr2ob  17602  drsdirfi  18351  toprntopon  23043  2ndcsb  23567  fbssint  23956  isfil2  23974  alexsubALTlem3  24167  lpbl  24621  metustfbas  24675  lrrecfr  28094  ex-natded9.26-2  30680  19.9d2rf  32726  rexunirn  32748  f1ocnt  33057  fsumiunle  33086  fmcncfil  34238  esumiun  34401  0elsiga  34421  ddemeas  34543  bnj168  35036  bnj593  35051  bnj607  35221  bnj600  35224  bnj916  35238  axprALT2  35417  fineqvpow  35423  tz9.1regs  35442  onvf1odlem1  35458  wevgblacfn  35466  lfuhgr3  35483  cusgredgex  35485  loop1cycl  35500  umgr2cycl  35504  fundmpss  36130  exisym1  36797  axtco2g  36850  bj-sylge  37091  bj-exextruan  37122  bj-cbvew  37126  bj-19.12  37210  bj-equs45fv  37308  bj-snsetex  37460  bj-snglss  37467  bj-snglex  37470  bj-bm1.3ii  37561  bj-axnul  37569  bj-axseprep  37571  bj-restn0  37592  bj-ccinftydisj  37717  mptsnunlem  37844  pibt2  37923  wl-cbvmotv  38028  wl-moae  38031  wl-nax6im  38033  eu6w  43270  iscard4  44121  ismnushort  44875  spsbce-2  44955  iotaexeu  44992  iotasbc  44993  relopabVD  45474  ax6e2ndeqVD  45482  2uasbanhVD  45484  ax6e2ndeqALT  45504  fnchoice  45607  rfcnnnub  45614  stoweidlem35  46607  stoweidlem57  46629  mo0sn  49445