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  nfexhe  2182  19.12  2332  ax13lem2  2380  exdistrf  2451  equs45f  2463  dfmoeu  2535  eu6  2574  2eu2ex  2643  reximi2  3069  cgsexg  3485  gencbvex  3499  eqvincg  3602  sbcg  3813  n0rex  4309  axrep2  5227  sepex  5245  bm1.3iiOLD  5247  ax6vsep  5248  copsexgw  5438  copsexg  5439  relopabi  5771  dmcoss  5924  dminss  6111  imainss  6112  iotanul2  6465  fv3  6852  ssimaex  6919  dffv2  6929  exfo  7050  oprabidw  7389  oprabid  7390  zfrep6  7899  frxp  8068  suppimacnvss  8115  tz7.48-1  8374  enssdom  8913  enssdomOLD  8914  enfii  9110  fineqvlem  9166  enp1i  9179  infcntss  9223  infeq5  9546  rankuni  9775  scott0  9798  acni3  9957  acnnum  9962  dfac3  10031  dfac9  10047  kmlem1  10061  cflm  10160  cfcof  10184  axdc4lem  10365  axcclem  10367  ac6c4  10391  ac6s  10394  ac6s2  10396  axdclem2  10430  brdom3  10438  brdom5  10439  brdom4  10440  nqpr  10925  ltexprlem4  10950  reclem2pr  10959  hash1to3  14415  trclublem  14918  fnpr2ob  17479  drsdirfi  18228  toprntopon  22869  2ndcsb  23393  fbssint  23782  isfil2  23800  alexsubALTlem3  23993  lpbl  24447  metustfbas  24501  lrrecfr  27939  ex-natded9.26-2  30495  19.9d2rf  32543  rexunirn  32566  f1ocnt  32880  fsumiunle  32910  fmcncfil  34088  esumiun  34251  0elsiga  34271  ddemeas  34393  bnj168  34886  bnj593  34901  bnj607  35072  bnj600  35075  bnj916  35089  fineqvpow  35271  tz9.1regs  35290  onvf1odlem1  35297  wevgblacfn  35303  lfuhgr3  35314  cusgredgex  35316  loop1cycl  35331  umgr2cycl  35335  fundmpss  35961  exisym1  36618  exeltr  36665  bj-sylge  36824  bj-19.12  36962  bj-equs45fv  37012  bj-snsetex  37164  bj-snglss  37171  bj-snglex  37174  bj-bm1.3ii  37265  bj-restn0  37291  bj-ccinftydisj  37414  mptsnunlem  37539  pibt2  37618  wl-cbvmotv  37714  wl-moae  37717  wl-nax6im  37719  eu6w  42915  iscard4  43770  ismnushort  44538  spsbce-2  44618  iotaexeu  44655  iotasbc  44656  relopabVD  45137  ax6e2ndeqVD  45145  2uasbanhVD  45147  ax6e2ndeqALT  45167  fnchoice  45270  rfcnnnub  45277  stoweidlem35  46275  stoweidlem57  46297  mo0sn  49057