Theorem eximi 1759

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

Syntax hints:   → wi 4  ∃wex 1701

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

This theorem depends on definitions:  df-bi 197  df-ex 1702

This theorem is referenced by:  2eximi  1760  eximii  1761  exa1  1762  exan  1786  exsimpl  1794  exsimpr  1795  19.29r2  1803  19.29x  1804  19.35  1805  19.40-2  1814  exlimiv  1860  speimfwALT  1879  sbimi  1888  19.12  2166  ax13lem2  2300  exdistrf  2337  equs45f  2354  mo2v  2481  2eu2ex  2550  reximi2  3009  cgsexg  3229  gencbvex  3241  vtocl3  3253  eqvinc  3318  n0rex  3916  axrep2  4738  bm1.3ii  4749  ax6vsep  4750  copsexg  4921  relopabi  5210  dminss  5510  imainss  5511  elsnxpOLD  5640  iotaex  5830  fv3  6164  ssimaex  6221  dffv2  6229  exfo  6334  oprabid  6632  zfrep6  7084  frxp  7233  suppimacnvss  7251  tz7.48-1  7484  enssdom  7925  fineqvlem  8119  infcntss  8179  infeq5  8479  omex  8485  rankuni  8671  scott0  8694  acni3  8815  acnnum  8820  dfac3  8889  dfac9  8903  kmlem1  8917  cflm  9017  cfcof  9041  axdc4lem  9222  axcclem  9224  ac6c4  9248  ac6s  9251  ac6s2  9253  axdclem2  9287  brdom3  9295  brdom5  9296  brdom4  9297  nqpr  9781  ltexprlem4  9806  reclem2pr  9815  hash1to3  13207  trclublem  13663  drsdirfi  16854  2ndcsb  21157  fbssint  21547  isfil2  21565  alexsubALTlem3  21758  lpbl  22213  metustfbas  22267  ex-natded9.26-2  27125  eqvincg  29154  19.9d2rf  29158  rexunirn  29171  f1ocnt  29392  fmcncfil  29751  esumiun  29929  0elsiga  29950  ddemeas  30072  bnj168  30498  bnj593  30515  bnj607  30686  bnj600  30689  bnj916  30703  fundmpss  31356  exisym1  32038  bj-exlime  32224  bj-sbex  32241  bj-ssbequ2  32258  bj-equs45fv  32368  bj-axrep2  32405  bj-eumo0  32446  bj-snsetex  32571  bj-snglss  32578  bj-snglex  32581  bj-restn0  32653  bj-toprntopon  32673  bj-ccinftydisj  32706  mptsnunlem  32790  spsbce-2  38029  iotaexeu  38068  iotasbc  38069  relopabVD  38587  ax6e2ndeqVD  38595  2uasbanhVD  38597  ax6e2ndeqALT  38617  fnchoice  38638  rfcnnnub  38645  stoweidlem35  39527  stoweidlem57  39549