Theorem eximi 1835

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 1834	. 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 209  df-ex 1781

This theorem is referenced by:  2eximi  1836  eximii  1837  exa1  1838  exsimpl  1869  exsimpr  1870  19.29r2  1876  19.29x  1877  19.35  1878  19.40-2  1888  emptyex  1908  exlimiv  1931  speimfwALT  1967  spsbeOLD  2089  19.12  2346  ax13lem2  2394  exdistrf  2469  equs45f  2482  sbimiOLD  2515  sbimiALT  2577  dfmoeu  2618  moimi  2627  eu6  2659  2eu2ex  2728  reximi2  3244  cgsexg  3537  gencbvex  3549  eqvincg  3641  n0rex  4314  axrep2  5193  bm1.3ii  5206  ax6vsep  5207  copsexgw  5381  copsexg  5382  relopabi  5694  dminss  6010  imainss  6011  iotaex  6335  fv3  6688  ssimaex  6748  dffv2  6756  exfo  6871  oprabidw  7187  oprabid  7188  zfrep6  7656  frxp  7820  suppimacnvss  7840  tz7.48-1  8079  enssdom  8534  fineqvlem  8732  infcntss  8792  infeq5  9100  omex  9106  rankuni  9292  scott0  9315  acni3  9473  acnnum  9478  dfac3  9547  dfac9  9562  kmlem1  9576  cflm  9672  cfcof  9696  axdc4lem  9877  axcclem  9879  ac6c4  9903  ac6s  9906  ac6s2  9908  axdclem2  9942  brdom3  9950  brdom5  9951  brdom4  9952  nqpr  10436  ltexprlem4  10461  reclem2pr  10470  hash1to3  13850  trclublem  14355  fnpr2ob  16831  drsdirfi  17548  toprntopon  21533  2ndcsb  22057  fbssint  22446  isfil2  22464  alexsubALTlem3  22657  lpbl  23113  metustfbas  23167  ex-natded9.26-2  28199  19.9d2rf  30235  rexunirn  30256  f1ocnt  30525  fsumiunle  30545  fmcncfil  31174  esumiun  31353  0elsiga  31373  ddemeas  31495  bnj168  32000  bnj593  32016  bnj607  32188  bnj600  32191  bnj916  32205  lfuhgr3  32366  cusgredgex  32368  loop1cycl  32384  umgr2cycl  32388  fundmpss  33009  exisym1  33772  bj-sylge  33957  bj-19.12  34090  bj-equs45fv  34133  bj-snsetex  34278  bj-snglss  34285  bj-snglex  34288  bj-bm1.3ii  34360  bj-restn0  34384  bj-ccinftydisj  34498  mptsnunlem  34622  pibt2  34701  wl-cbvmotv  34768  wl-moae  34771  wl-nax6im  34773  iscard4  39920  spsbce-2  40733  iotaexeu  40770  iotasbc  40771  relopabVD  41255  ax6e2ndeqVD  41263  2uasbanhVD  41265  ax6e2ndeqALT  41285  fnchoice  41306  rfcnnnub  41313  stoweidlem35  42340  stoweidlem57  42362