Theorem eximi 1836

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

Syntax hints:   → wi 4  ∃wex 1780

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

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

This theorem is referenced by:  2eximi  1837  eximii  1838  exa1  1839  exsimpl  1869  exsimpr  1870  19.29r2  1876  19.29x  1877  19.35  1878  19.40-2  1888  emptyex  1908  exlimiv  1931  speimfwALT  1965  19.12  2328  ax13lem2  2376  exdistrf  2447  equs45f  2459  dfmoeu  2531  moimi  2540  eu6  2569  2eu2ex  2638  reximi2  3065  cgsexg  3481  gencbvex  3496  eqvincg  3603  sbcg  3814  n0rex  4307  axrep2  5220  sepex  5238  bm1.3iiOLD  5240  ax6vsep  5241  copsexgw  5430  copsexg  5431  relopabi  5762  dmcoss  5914  dminss  6100  imainss  6101  iotanul2  6454  fv3  6840  ssimaex  6907  dffv2  6917  exfo  7038  oprabidw  7377  oprabid  7378  zfrep6  7887  frxp  8056  suppimacnvss  8103  tz7.48-1  8362  enssdom  8899  enfii  9095  fineqvlem  9150  enp1i  9163  infcntss  9207  infeq5  9527  rankuni  9753  scott0  9776  acni3  9935  acnnum  9940  dfac3  10009  dfac9  10025  kmlem1  10039  cflm  10138  cfcof  10162  axdc4lem  10343  axcclem  10345  ac6c4  10369  ac6s  10372  ac6s2  10374  axdclem2  10408  brdom3  10416  brdom5  10417  brdom4  10418  nqpr  10902  ltexprlem4  10927  reclem2pr  10936  hash1to3  14396  trclublem  14899  fnpr2ob  17459  drsdirfi  18208  toprntopon  22838  2ndcsb  23362  fbssint  23751  isfil2  23769  alexsubALTlem3  23962  lpbl  24416  metustfbas  24470  lrrecfr  27884  ex-natded9.26-2  30395  19.9d2rf  32443  rexunirn  32466  f1ocnt  32777  fsumiunle  32807  fmcncfil  33939  esumiun  34102  0elsiga  34122  ddemeas  34244  bnj168  34737  bnj593  34752  bnj607  34923  bnj600  34926  bnj916  34940  tz9.1regs  35118  fineqvpow  35126  onvf1odlem1  35135  wevgblacfn  35141  lfuhgr3  35152  cusgredgex  35154  loop1cycl  35169  umgr2cycl  35173  fundmpss  35799  exisym1  36457  bj-sylge  36657  bj-19.12  36794  bj-equs45fv  36844  bj-snsetex  36996  bj-snglss  37003  bj-snglex  37006  bj-bm1.3ii  37097  bj-restn0  37123  bj-ccinftydisj  37246  mptsnunlem  37371  pibt2  37450  wl-cbvmotv  37546  wl-moae  37549  wl-nax6im  37551  eu6w  42708  iscard4  43565  ismnushort  44333  spsbce-2  44413  iotaexeu  44450  iotasbc  44451  relopabVD  44932  ax6e2ndeqVD  44940  2uasbanhVD  44942  ax6e2ndeqALT  44962  fnchoice  45065  rfcnnnub  45072  stoweidlem35  46072  stoweidlem57  46094  mo0sn  48846