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  2328  ax13lem2  2381  exdistrf  2452  equs45f  2464  dfmoeu  2536  moimi  2545  eu6  2574  2eu2ex  2643  reximi2  3070  cgsexg  3510  gencbvex  3525  eqvincg  3632  sbcg  3843  n0rex  4337  axrep2  5257  sepex  5275  bm1.3iiOLD  5277  ax6vsep  5278  copsexgw  5470  copsexg  5471  relopabi  5806  dminss  6147  imainss  6148  iotanul2  6506  iotaexOLD  6516  fv3  6899  ssimaex  6969  dffv2  6979  exfo  7100  oprabidw  7441  oprabid  7442  zfrep6  7958  frxp  8130  suppimacnvss  8177  tz7.48-1  8462  enssdom  8996  enfii  9205  fineqvlem  9275  enp1i  9290  infcntss  9339  infeq5  9656  rankuni  9882  scott0  9905  acni3  10066  acnnum  10071  dfac3  10140  dfac9  10156  kmlem1  10170  cflm  10269  cfcof  10293  axdc4lem  10474  axcclem  10476  ac6c4  10500  ac6s  10503  ac6s2  10505  axdclem2  10539  brdom3  10547  brdom5  10548  brdom4  10549  nqpr  11033  ltexprlem4  11058  reclem2pr  11067  hash1to3  14515  trclublem  15019  fnpr2ob  17577  drsdirfi  18322  toprntopon  22868  2ndcsb  23392  fbssint  23781  isfil2  23799  alexsubALTlem3  23992  lpbl  24447  metustfbas  24501  lrrecfr  27907  ex-natded9.26-2  30406  19.9d2rf  32455  rexunirn  32478  f1ocnt  32784  fsumiunle  32813  fmcncfil  33967  esumiun  34130  0elsiga  34150  ddemeas  34272  bnj168  34766  bnj593  34781  bnj607  34952  bnj600  34955  bnj916  34969  fineqvpow  35132  wevgblacfn  35136  lfuhgr3  35147  cusgredgex  35149  loop1cycl  35164  umgr2cycl  35168  fundmpss  35789  exisym1  36447  bj-sylge  36647  bj-19.12  36784  bj-equs45fv  36834  bj-snsetex  36986  bj-snglss  36993  bj-snglex  36996  bj-bm1.3ii  37087  bj-restn0  37113  bj-ccinftydisj  37236  mptsnunlem  37361  pibt2  37440  wl-cbvmotv  37536  wl-moae  37539  wl-nax6im  37541  eu6w  42674  iscard4  43532  ismnushort  44300  spsbce-2  44380  iotaexeu  44417  iotasbc  44418  relopabVD  44900  ax6e2ndeqVD  44908  2uasbanhVD  44910  ax6e2ndeqALT  44930  fnchoice  45033  rfcnnnub  45040  stoweidlem35  46044  stoweidlem57  46066  mo0sn  48774