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  2330  ax13lem2  2378  exdistrf  2449  equs45f  2461  dfmoeu  2533  moimi  2542  eu6  2571  2eu2ex  2640  reximi2  3066  cgsexg  3482  gencbvex  3496  eqvincg  3599  sbcg  3810  n0rex  4306  axrep2  5222  sepex  5240  bm1.3iiOLD  5242  ax6vsep  5243  copsexgw  5433  copsexg  5434  relopabi  5766  dmcoss  5918  dminss  6105  imainss  6106  iotanul2  6459  fv3  6846  ssimaex  6913  dffv2  6923  exfo  7044  oprabidw  7383  oprabid  7384  zfrep6  7893  frxp  8062  suppimacnvss  8109  tz7.48-1  8368  enssdom  8905  enssdomOLD  8906  enfii  9102  fineqvlem  9157  enp1i  9170  infcntss  9214  infeq5  9534  rankuni  9763  scott0  9786  acni3  9945  acnnum  9950  dfac3  10019  dfac9  10035  kmlem1  10049  cflm  10148  cfcof  10172  axdc4lem  10353  axcclem  10355  ac6c4  10379  ac6s  10382  ac6s2  10384  axdclem2  10418  brdom3  10426  brdom5  10427  brdom4  10428  nqpr  10912  ltexprlem4  10937  reclem2pr  10946  hash1to3  14401  trclublem  14904  fnpr2ob  17464  drsdirfi  18213  toprntopon  22841  2ndcsb  23365  fbssint  23754  isfil2  23772  alexsubALTlem3  23965  lpbl  24419  metustfbas  24473  lrrecfr  27887  ex-natded9.26-2  30402  19.9d2rf  32450  rexunirn  32473  f1ocnt  32787  fsumiunle  32817  fmcncfil  33965  esumiun  34128  0elsiga  34148  ddemeas  34270  bnj168  34763  bnj593  34778  bnj607  34949  bnj600  34952  bnj916  34966  tz9.1regs  35151  fineqvpow  35159  onvf1odlem1  35168  wevgblacfn  35174  lfuhgr3  35185  cusgredgex  35187  loop1cycl  35202  umgr2cycl  35206  fundmpss  35832  exisym1  36489  bj-sylge  36689  bj-19.12  36826  bj-equs45fv  36876  bj-snsetex  37028  bj-snglss  37035  bj-snglex  37038  bj-bm1.3ii  37129  bj-restn0  37155  bj-ccinftydisj  37278  mptsnunlem  37403  pibt2  37482  wl-cbvmotv  37578  wl-moae  37581  wl-nax6im  37583  nfexhe  42327  eu6w  42794  iscard4  43650  ismnushort  44418  spsbce-2  44498  iotaexeu  44535  iotasbc  44536  relopabVD  45017  ax6e2ndeqVD  45025  2uasbanhVD  45027  ax6e2ndeqALT  45047  fnchoice  45150  rfcnnnub  45157  stoweidlem35  46157  stoweidlem57  46179  mo0sn  48940