Theorem eximi 1878

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

Syntax hints:   → wi 4  ∃wex 1823

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

This theorem depends on definitions:  df-bi 199  df-ex 1824

This theorem is referenced by:  2eximi  1879  eximii  1880  exa1  1881  exanOLD  1907  exsimpl  1913  exsimpr  1914  19.29r2  1922  19.29x  1923  19.35  1924  19.40-2  1933  exlimiv  1973  speimfwALT  2008  sbimi  2017  19.12  2303  ax13lem2  2338  exdistrf  2413  equs45f  2425  moimi  2557  dfmo  2615  2eu2ex  2673  reximi2  3191  cgsexg  3440  gencbvex  3452  vtocl3  3463  eqvincg  3532  n0rex  4163  axrep2  5011  bm1.3ii  5022  ax6vsep  5023  copsexg  5189  relopabi  5493  dminss  5803  imainss  5804  iotaex  6118  fv3  6466  ssimaex  6525  dffv2  6533  exfo  6643  oprabid  6955  zfrep6  7415  frxp  7570  suppimacnvss  7588  tz7.48-1  7823  enssdom  8268  fineqvlem  8464  infcntss  8524  infeq5  8833  omex  8839  rankuni  9025  scott0  9048  acni3  9205  acnnum  9210  dfac3  9279  dfac9  9295  kmlem1  9309  cflm  9409  cfcof  9433  axdc4lem  9614  axcclem  9616  ac6c4  9640  ac6s  9643  ac6s2  9645  axdclem2  9679  brdom3  9687  brdom5  9688  brdom4  9689  nqpr  10173  ltexprlem4  10198  reclem2pr  10207  hash1to3  13593  trclublem  14149  drsdirfi  17335  toprntopon  21148  2ndcsb  21672  fbssint  22061  isfil2  22079  alexsubALTlem3  22272  lpbl  22727  metustfbas  22781  ex-natded9.26-2  27869  19.9d2rf  29907  rexunirn  29915  iunrnmptss  29963  f1ocnt  30137  fsumiunle  30153  fmcncfil  30583  esumiun  30762  0elsiga  30783  ddemeas  30905  bnj168  31406  bnj593  31422  bnj607  31593  bnj600  31596  bnj916  31610  fundmpss  32265  exisym1  33014  bj-exlime  33196  bj-sbex  33225  bj-ssbequ2  33241  bj-equs45fv  33345  bj-axrep2  33374  bj-snsetex  33531  bj-snglss  33538  bj-snglex  33541  bj-bm1.3ii  33604  bj-restn0  33624  bj-ccinftydisj  33698  mptsnunlem  33788  wl-cbvmotv  33898  wl-moae  33901  wl-nax6im  33903  wl-nax6al  33904  spsbce-2  39550  iotaexeu  39588  iotasbc  39589  relopabVD  40084  ax6e2ndeqVD  40092  2uasbanhVD  40094  ax6e2ndeqALT  40114  fnchoice  40135  rfcnnnub  40142  stoweidlem35  41193  stoweidlem57  41215