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 1799	1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1781

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

This theorem depends on definitions:  df-bi 210  df-ex 1782

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  1967  19.12  2335  ax13lem2  2383  exdistrf  2458  equs45f  2471  sbimiALT  2553  dfmoeu  2594  moimi  2603  eu6  2634  2eu2ex  2705  reximi2  3207  cgsexg  3484  gencbvex  3497  eqvincg  3589  n0rex  4268  axrep2  5157  bm1.3ii  5170  ax6vsep  5171  copsexgw  5346  copsexg  5347  relopabi  5658  dminss  5977  imainss  5978  iotaex  6304  fv3  6663  ssimaex  6723  dffv2  6733  exfo  6848  oprabidw  7166  oprabid  7167  zfrep6  7638  frxp  7803  suppimacnvss  7823  tz7.48-1  8062  enssdom  8517  fineqvlem  8716  infcntss  8776  infeq5  9084  omex  9090  rankuni  9276  scott0  9299  acni3  9458  acnnum  9463  dfac3  9532  dfac9  9547  kmlem1  9561  cflm  9661  cfcof  9685  axdc4lem  9866  axcclem  9868  ac6c4  9892  ac6s  9895  ac6s2  9897  axdclem2  9931  brdom3  9939  brdom5  9940  brdom4  9941  nqpr  10425  ltexprlem4  10450  reclem2pr  10459  hash1to3  13845  trclublem  14346  fnpr2ob  16823  drsdirfi  17540  toprntopon  21530  2ndcsb  22054  fbssint  22443  isfil2  22461  alexsubALTlem3  22654  lpbl  23110  metustfbas  23164  ex-natded9.26-2  28205  19.9d2rf  30242  rexunirn  30263  f1ocnt  30551  fsumiunle  30571  fmcncfil  31284  esumiun  31463  0elsiga  31483  ddemeas  31605  bnj168  32110  bnj593  32126  bnj607  32298  bnj600  32301  bnj916  32315  lfuhgr3  32479  cusgredgex  32481  loop1cycl  32497  umgr2cycl  32501  fundmpss  33122  exisym1  33885  bj-sylge  34070  bj-19.12  34205  bj-equs45fv  34248  bj-snsetex  34399  bj-snglss  34406  bj-snglex  34409  bj-bm1.3ii  34481  bj-restn0  34505  bj-ccinftydisj  34628  mptsnunlem  34755  pibt2  34834  wl-cbvmotv  34918  wl-moae  34921  wl-nax6im  34923  iscard4  40241  spsbce-2  41085  iotaexeu  41122  iotasbc  41123  relopabVD  41607  ax6e2ndeqVD  41615  2uasbanhVD  41617  ax6e2ndeqALT  41637  fnchoice  41658  rfcnnnub  41665  stoweidlem35  42677  stoweidlem57  42699