Theorem eximi 1837

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

Syntax hints:   → wi 4  ∃wex 1781

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

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

This theorem is referenced by:  2eximi  1838  eximii  1839  exa1  1840  exsimpl  1870  exsimpr  1871  19.29r2  1877  19.29x  1878  19.35  1879  19.40-2  1889  emptyex  1909  exlimiv  1932  speimfwALT  1966  nfexhe  2183  19.12  2333  ax13lem2  2381  exdistrf  2452  equs45f  2464  dfmoeu  2536  eu6  2575  2eu2ex  2644  reximi2  3071  cgsexg  3487  gencbvex  3501  eqvincg  3604  sbcg  3815  n0rex  4311  axrep2  5229  sepex  5247  bm1.3iiOLD  5249  ax6vsep  5250  axprg  5383  copsexgw  5446  copsexg  5447  relopabi  5779  dmcoss  5932  dminss  6119  imainss  6120  iotanul2  6473  fv3  6860  ssimaex  6927  dffv2  6937  exfo  7059  oprabidw  7399  oprabid  7400  zfrep6  7909  frxp  8078  suppimacnvss  8125  tz7.48-1  8384  enssdom  8925  enssdomOLD  8926  enfii  9122  fineqvlem  9178  enp1i  9191  infcntss  9235  infeq5  9558  rankuni  9787  scott0  9810  acni3  9969  acnnum  9974  dfac3  10043  dfac9  10059  kmlem1  10073  cflm  10172  cfcof  10196  axdc4lem  10377  axcclem  10379  ac6c4  10403  ac6s  10406  ac6s2  10408  axdclem2  10442  brdom3  10450  brdom5  10451  brdom4  10452  nqpr  10937  ltexprlem4  10962  reclem2pr  10971  hash1to3  14427  trclublem  14930  fnpr2ob  17491  drsdirfi  18240  toprntopon  22881  2ndcsb  23405  fbssint  23794  isfil2  23812  alexsubALTlem3  24005  lpbl  24459  metustfbas  24513  lrrecfr  27951  ex-natded9.26-2  30507  19.9d2rf  32554  rexunirn  32577  f1ocnt  32890  fsumiunle  32920  fmcncfil  34108  esumiun  34271  0elsiga  34291  ddemeas  34413  bnj168  34906  bnj593  34921  bnj607  35091  bnj600  35094  bnj916  35108  fineqvpow  35290  tz9.1regs  35309  onvf1odlem1  35316  wevgblacfn  35322  lfuhgr3  35333  cusgredgex  35335  loop1cycl  35350  umgr2cycl  35354  fundmpss  35980  exisym1  36637  exeltr  36684  bj-sylge  36851  bj-exextruan  36875  bj-cbvew  36879  bj-19.12  36960  bj-equs45fv  37053  bj-snsetex  37205  bj-snglss  37212  bj-snglex  37215  bj-bm1.3ii  37306  bj-axnul  37314  bj-axseprep  37316  bj-restn0  37337  bj-ccinftydisj  37462  mptsnunlem  37587  pibt2  37666  wl-cbvmotv  37762  wl-moae  37765  wl-nax6im  37767  eu6w  43028  iscard4  43883  ismnushort  44651  spsbce-2  44731  iotaexeu  44768  iotasbc  44769  relopabVD  45250  ax6e2ndeqVD  45258  2uasbanhVD  45260  ax6e2ndeqALT  45280  fnchoice  45383  rfcnnnub  45390  stoweidlem35  46387  stoweidlem57  46409  mo0sn  49169