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

Syntax hints:   → wi 4  ∃wex 1779

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

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  2eximi  1836  eximii  1837  exa1  1838  exsimpl  1868  exsimpr  1869  19.29r2  1875  19.29x  1876  19.35  1877  19.40-2  1887  emptyex  1907  exlimiv  1930  speimfwALT  1964  19.12  2326  ax13lem2  2374  exdistrf  2445  equs45f  2457  dfmoeu  2529  moimi  2538  eu6  2567  2eu2ex  2636  reximi2  3062  cgsexg  3481  gencbvex  3496  eqvincg  3603  sbcg  3815  n0rex  4308  axrep2  5221  sepex  5239  bm1.3iiOLD  5241  ax6vsep  5242  copsexgw  5433  copsexg  5434  relopabi  5765  dmcoss  5916  dminss  6102  imainss  6103  iotanul2  6455  fv3  6840  ssimaex  6908  dffv2  6918  exfo  7039  oprabidw  7380  oprabid  7381  zfrep6  7890  frxp  8059  suppimacnvss  8106  tz7.48-1  8365  enssdom  8902  enfii  9100  fineqvlem  9155  enp1i  9168  infcntss  9212  infeq5  9533  rankuni  9759  scott0  9782  acni3  9941  acnnum  9946  dfac3  10015  dfac9  10031  kmlem1  10045  cflm  10144  cfcof  10168  axdc4lem  10349  axcclem  10351  ac6c4  10375  ac6s  10378  ac6s2  10380  axdclem2  10414  brdom3  10422  brdom5  10423  brdom4  10424  nqpr  10908  ltexprlem4  10933  reclem2pr  10942  hash1to3  14399  trclublem  14902  fnpr2ob  17462  drsdirfi  18211  toprntopon  22810  2ndcsb  23334  fbssint  23723  isfil2  23741  alexsubALTlem3  23934  lpbl  24389  metustfbas  24443  lrrecfr  27857  ex-natded9.26-2  30368  19.9d2rf  32417  rexunirn  32440  f1ocnt  32754  fsumiunle  32783  fmcncfil  33914  esumiun  34077  0elsiga  34097  ddemeas  34219  bnj168  34713  bnj593  34728  bnj607  34899  bnj600  34902  bnj916  34916  tz9.1regs  35083  fineqvpow  35087  onvf1odlem1  35096  wevgblacfn  35102  lfuhgr3  35113  cusgredgex  35115  loop1cycl  35130  umgr2cycl  35134  fundmpss  35760  exisym1  36418  bj-sylge  36618  bj-19.12  36755  bj-equs45fv  36805  bj-snsetex  36957  bj-snglss  36964  bj-snglex  36967  bj-bm1.3ii  37058  bj-restn0  37084  bj-ccinftydisj  37207  mptsnunlem  37332  pibt2  37411  wl-cbvmotv  37507  wl-moae  37510  wl-nax6im  37512  eu6w  42669  iscard4  43526  ismnushort  44294  spsbce-2  44374  iotaexeu  44411  iotasbc  44412  relopabVD  44894  ax6e2ndeqVD  44902  2uasbanhVD  44904  ax6e2ndeqALT  44924  fnchoice  45027  rfcnnnub  45034  stoweidlem35  46036  stoweidlem57  46058  mo0sn  48820