Theorem eximi 1842

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 1841	. 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 208  df-ex 1787

This theorem is referenced by:  2eximi  1843  eximii  1844  exa1  1845  exsimpl  1875  exsimpr  1876  19.29r2  1882  19.29x  1883  19.35  1884  19.40-2  1894  emptyex  1914  exlimiv  1937  speimfwALT  1971  nfexhe  2187  19.12  2336  ax13lem2  2384  exdistrf  2455  equs45f  2467  dfmoeu  2539  eu6  2578  2eu2ex  2647  reximi2  3073  cgsexg  3477  gencbvex  3490  eqvincg  3593  sbcg  3802  n0rex  4292  axrep2  5209  sepex  5229  bm1.3iiOLD  5231  ax6vsep  5232  axprg  5373  copsexgwOLD  5438  copsexg  5439  relopabi  5772  dmcoss  5924  dminss  6111  imainss  6112  iotanul2  6465  fv3  6852  ssimaex  6919  dffv2  6929  exfo  7053  oprabidw  7394  oprabid  7395  zfrep6OLD  7904  frxp  8073  suppimacnvss  8120  tz7.48-1  8379  enssdom  8920  enssdomOLD  8921  enfii  9117  fineqvlem  9173  enp1i  9186  infcntss  9230  infeq5  9556  rankuni  9785  scott0  9808  acni3  9967  acnnum  9972  dfac3  10041  dfac9  10057  kmlem1  10071  cflm  10170  cfcof  10194  axdc4lem  10375  axcclem  10377  ac6c4  10401  ac6s  10404  ac6s2  10406  axdclem2  10440  brdom3  10448  brdom5  10449  brdom4  10450  nqpr  10935  ltexprlem4  10960  reclem2pr  10969  hash1to3  14452  trclublem  14955  fnpr2ob  17520  drsdirfi  18269  toprntopon  22915  2ndcsb  23439  fbssint  23828  isfil2  23846  alexsubALTlem3  24039  lpbl  24493  metustfbas  24547  lrrecfr  27960  ex-natded9.26-2  30515  19.9d2rf  32563  rexunirn  32586  f1ocnt  32899  fsumiunle  32928  fmcncfil  34122  esumiun  34285  0elsiga  34305  ddemeas  34427  bnj168  34920  bnj593  34935  bnj607  35105  bnj600  35108  bnj916  35122  axprALT2  35297  fineqvpow  35303  tz9.1regs  35322  onvf1odlem1  35338  wevgblacfn  35344  lfuhgr3  35355  cusgredgex  35357  loop1cycl  35372  umgr2cycl  35376  fundmpss  36002  exisym1  36659  axtco2g  36712  bj-sylge  36954  bj-exextruan  36985  bj-cbvew  36989  bj-19.12  37073  bj-equs45fv  37171  bj-snsetex  37323  bj-snglss  37330  bj-snglex  37333  bj-bm1.3ii  37424  bj-axnul  37432  bj-axseprep  37434  bj-restn0  37455  bj-ccinftydisj  37580  mptsnunlem  37707  pibt2  37786  wl-cbvmotv  37891  wl-moae  37894  wl-nax6im  37896  eu6w  43133  iscard4  43984  ismnushort  44752  spsbce-2  44832  iotaexeu  44869  iotasbc  44870  relopabVD  45351  ax6e2ndeqVD  45359  2uasbanhVD  45361  ax6e2ndeqALT  45381  fnchoice  45484  rfcnnnub  45491  stoweidlem35  46485  stoweidlem57  46507  mo0sn  49313