Theorem eximi 1802

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

Syntax hints:   → wi 4  ∃wex 1744

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

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

This theorem is referenced by:  2eximi  1803  eximii  1804  exa1  1805  exan  1828  exsimpl  1835  exsimpr  1836  19.29r2  1843  19.29x  1844  19.35  1845  19.40-2  1854  exlimiv  1898  speimfwALT  1934  sbimi  1943  19.12  2200  ax13lem2  2332  exdistrf  2364  equs45f  2378  mo2v  2505  2eu2ex  2575  reximi2  3039  cgsexg  3269  gencbvex  3281  vtocl3  3293  eqvincg  3360  n0rex  3968  axrep2  4806  bm1.3ii  4817  ax6vsep  4818  copsexg  4985  relopabi  5278  dminss  5582  imainss  5583  elsnxpOLD  5716  iotaex  5906  fv3  6244  ssimaex  6302  dffv2  6310  exfo  6417  oprabid  6717  zfrep6  7176  frxp  7332  suppimacnvss  7350  tz7.48-1  7583  enssdom  8022  fineqvlem  8215  infcntss  8275  infeq5  8572  omex  8578  rankuni  8764  scott0  8787  acni3  8908  acnnum  8913  dfac3  8982  dfac9  8996  kmlem1  9010  cflm  9110  cfcof  9134  axdc4lem  9315  axcclem  9317  ac6c4  9341  ac6s  9344  ac6s2  9346  axdclem2  9380  brdom3  9388  brdom5  9389  brdom4  9390  nqpr  9874  ltexprlem4  9899  reclem2pr  9908  hash1to3  13311  trclublem  13780  drsdirfi  16985  toprntopon  20777  2ndcsb  21300  fbssint  21689  isfil2  21707  alexsubALTlem3  21900  lpbl  22355  metustfbas  22409  ex-natded9.26-2  27407  19.9d2rf  29446  rexunirn  29458  f1ocnt  29687  fsumiunle  29703  fmcncfil  30105  esumiun  30284  0elsiga  30305  ddemeas  30427  bnj168  30924  bnj593  30941  bnj607  31112  bnj600  31115  bnj916  31129  fundmpss  31790  exisym1  32548  bj-exlime  32734  bj-sbex  32751  bj-ssbequ2  32768  bj-equs45fv  32877  bj-axrep2  32914  bj-eumo0  32955  bj-snsetex  33076  bj-snglss  33083  bj-snglex  33086  bj-restn0  33168  bj-ccinftydisj  33230  mptsnunlem  33315  spsbce-2  38897  iotaexeu  38936  iotasbc  38937  relopabVD  39451  ax6e2ndeqVD  39459  2uasbanhVD  39461  ax6e2ndeqALT  39481  fnchoice  39502  rfcnnnub  39509  stoweidlem35  40570  stoweidlem57  40592