Theorem eximi 1854

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

Syntax hints:   → wi 4  ∃wex 1798

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

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  2eximi  1855  eximii  1856  exa1  1857  exsimpl  1887  exsimpr  1888  19.29r2  1894  19.29x  1895  19.35  1896  19.40-2  1906  emptyex  1926  exlimiv  1949  speimfwALT  1983  nfexhe  2209  19.12  2358  ax13lem2  2406  exdistrf  2477  equs45f  2489  dfmoeu  2561  eu6  2600  2eu2ex  2669  reximi2  3094  cgsexg  3497  gencbvex  3509  eqvincg  3607  sbcg  3816  n0rex  4309  axrep2  5229  sepex  5249  bm1.3iiOLD  5251  ax6vsep  5252  axprg  5393  copsexgwOLD  5458  copsexg  5459  relopabi  5793  dmcoss  5949  dminss  6135  imainss  6136  iotanul2  6490  fv3  6881  ssimaex  6948  dffv2  6958  exfo  7082  oprabidw  7423  oprabid  7424  zfrep6OLD  7932  frxp  8101  suppimacnvss  8148  tz7.48-1  8409  enssdom  8953  enssdomOLD  8954  enfii  9150  fineqvlem  9206  enp1i  9219  infcntss  9263  infeq5  9589  rankuni  9818  scott0  9841  acni3  10000  acnnum  10005  dfac3  10074  dfac9  10090  kmlem1  10104  cflm  10203  cfcof  10228  axdc4lem  10409  axcclem  10411  ac6c4  10435  ac6s  10438  ac6s2  10440  axdclem2  10474  brdom3  10482  brdom5  10483  brdom4  10484  nqpr  10969  ltexprlem4  10994  reclem2pr  11003  hash1to3  14502  trclublem  15005  fnpr2ob  17571  drsdirfi  18320  toprntopon  22965  2ndcsb  23489  fbssint  23878  isfil2  23896  alexsubALTlem3  24089  lpbl  24543  metustfbas  24597  lrrecfr  28013  ex-natded9.26-2  30568  19.9d2rf  32616  rexunirn  32639  f1ocnt  32952  fsumiunle  32981  fmcncfil  34189  esumiun  34352  0elsiga  34372  ddemeas  34494  bnj168  34990  bnj593  35005  bnj607  35175  bnj600  35178  bnj916  35192  axprALT2  35369  fineqvpow  35375  tz9.1regs  35394  onvf1odlem1  35410  wevgblacfn  35418  lfuhgr3  35434  cusgredgex  35436  loop1cycl  35451  umgr2cycl  35455  fundmpss  36081  exisym1  36748  axtco2g  36801  bj-sylge  37043  bj-exextruan  37074  bj-cbvew  37078  bj-19.12  37162  bj-equs45fv  37260  bj-snsetex  37412  bj-snglss  37419  bj-snglex  37422  bj-bm1.3ii  37513  bj-axnul  37521  bj-axseprep  37523  bj-restn0  37544  bj-ccinftydisj  37669  mptsnunlem  37796  pibt2  37875  wl-cbvmotv  37980  wl-moae  37983  wl-nax6im  37985  eu6w  43222  iscard4  44073  ismnushort  44841  spsbce-2  44921  iotaexeu  44958  iotasbc  44959  relopabVD  45440  ax6e2ndeqVD  45448  2uasbanhVD  45450  ax6e2ndeqALT  45470  fnchoice  45573  rfcnnnub  45580  stoweidlem35  46573  stoweidlem57  46595  mo0sn  49401