Theorem eximi 1841

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

Syntax hints:   → wi 4  ∃wex 1786

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

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

This theorem is referenced by:  2eximi  1842  eximii  1843  exa1  1844  exsimpl  1874  exsimpr  1875  19.29r2  1881  19.29x  1882  19.35  1883  19.40-2  1893  emptyex  1913  exlimiv  1936  speimfwALT  1971  19.12  2328  ax13lem2  2375  exdistrf  2446  equs45f  2458  dfmoeu  2536  moimi  2545  eu6  2575  2eu2ex  2646  reximi2  3157  cgsexg  3439  gencbvex  3452  eqvincg  3542  n0rex  4241  axrep2  5154  bm1.3ii  5167  ax6vsep  5168  copsexgw  5344  copsexg  5345  relopabi  5660  dminss  5979  imainss  5980  iotaex  6313  fv3  6686  ssimaex  6747  dffv2  6757  exfo  6875  oprabidw  7195  oprabid  7196  zfrep6  7674  frxp  7839  suppimacnvss  7861  tz7.48-1  8101  enssdom  8573  enfii  8777  fineqvlem  8804  infcntss  8859  infeq5  9166  omex  9172  rankuni  9358  scott0  9381  acni3  9540  acnnum  9545  dfac3  9614  dfac9  9629  kmlem1  9643  cflm  9743  cfcof  9767  axdc4lem  9948  axcclem  9950  ac6c4  9974  ac6s  9977  ac6s2  9979  axdclem2  10013  brdom3  10021  brdom5  10022  brdom4  10023  nqpr  10507  ltexprlem4  10532  reclem2pr  10541  hash1to3  13936  trclublem  14437  fnpr2ob  16927  drsdirfi  17657  toprntopon  21669  2ndcsb  22193  fbssint  22582  isfil2  22600  alexsubALTlem3  22793  lpbl  23249  metustfbas  23303  ex-natded9.26-2  28349  19.9d2rf  30386  rexunirn  30406  f1ocnt  30690  fsumiunle  30710  fmcncfil  31445  esumiun  31624  0elsiga  31644  ddemeas  31766  bnj168  32271  bnj593  32287  bnj607  32459  bnj600  32462  bnj916  32476  fineqvpow  32628  lfuhgr3  32644  cusgredgex  32646  loop1cycl  32662  umgr2cycl  32666  fundmpss  33304  lrrecfr  33729  exisym1  34243  bj-sylge  34432  bj-19.12  34570  bj-equs45fv  34613  bj-snsetex  34765  bj-snglss  34772  bj-snglex  34775  bj-bm1.3ii  34847  bj-restn0  34871  bj-ccinftydisj  34994  mptsnunlem  35121  pibt2  35200  wl-cbvmotv  35284  wl-moae  35287  wl-nax6im  35289  iscard4  40678  spsbce-2  41521  iotaexeu  41558  iotasbc  41559  relopabVD  42043  ax6e2ndeqVD  42051  2uasbanhVD  42053  ax6e2ndeqALT  42073  fnchoice  42094  rfcnnnub  42101  stoweidlem35  43102  stoweidlem57  43124  mo0sn  45677