Theorem eximi 1838

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

Syntax hints:   → wi 4  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  2eximi  1839  eximii  1840  exa1  1841  exsimpl  1872  exsimpr  1873  19.29r2  1879  19.29x  1880  19.35  1881  19.40-2  1891  emptyex  1911  exlimiv  1934  speimfwALT  1969  19.12  2321  ax13lem2  2376  exdistrf  2447  equs45f  2459  dfmoeu  2531  moimi  2540  eu6  2569  2eu2ex  2640  reximi2  3080  cgsexg  3519  gencbvex  3536  eqvincg  3636  sbcg  3856  n0rex  4354  axrep2  5288  bm1.3ii  5302  ax6vsep  5303  copsexgw  5490  copsexg  5491  relopabi  5821  dminss  6150  imainss  6151  iotanul2  6511  iotaexOLD  6521  fv3  6907  ssimaex  6974  dffv2  6984  exfo  7104  oprabidw  7437  oprabid  7438  zfrep6  7938  frxp  8109  suppimacnvss  8155  tz7.48-1  8440  enssdom  8970  enfii  9186  fineqvlem  9259  enp1i  9276  infcntss  9318  infeq5  9629  omex  9635  rankuni  9855  scott0  9878  acni3  10039  acnnum  10044  dfac3  10113  dfac9  10128  kmlem1  10142  cflm  10242  cfcof  10266  axdc4lem  10447  axcclem  10449  ac6c4  10473  ac6s  10476  ac6s2  10478  axdclem2  10512  brdom3  10520  brdom5  10521  brdom4  10522  nqpr  11006  ltexprlem4  11031  reclem2pr  11040  hash1to3  14449  trclublem  14939  fnpr2ob  17501  drsdirfi  18255  toprntopon  22419  2ndcsb  22945  fbssint  23334  isfil2  23352  alexsubALTlem3  23545  lpbl  24004  metustfbas  24058  lrrecfr  27417  ex-natded9.26-2  29663  19.9d2rf  31699  rexunirn  31720  f1ocnt  32001  fsumiunle  32023  fmcncfil  32900  esumiun  33081  0elsiga  33101  ddemeas  33223  bnj168  33730  bnj593  33745  bnj607  33916  bnj600  33919  bnj916  33933  fineqvpow  34085  lfuhgr3  34099  cusgredgex  34101  loop1cycl  34117  umgr2cycl  34121  fundmpss  34727  exisym1  35298  bj-sylge  35490  bj-19.12  35628  bj-equs45fv  35678  bj-snsetex  35833  bj-snglss  35840  bj-snglex  35843  bj-bm1.3ii  35934  bj-restn0  35960  bj-ccinftydisj  36083  mptsnunlem  36208  pibt2  36287  wl-cbvmotv  36371  wl-moae  36374  wl-nax6im  36376  iscard4  42270  ismnushort  43046  spsbce-2  43126  iotaexeu  43163  iotasbc  43164  relopabVD  43648  ax6e2ndeqVD  43656  2uasbanhVD  43658  ax6e2ndeqALT  43678  fnchoice  43699  rfcnnnub  43706  stoweidlem35  44738  stoweidlem57  44760  mo0sn  47454