Theorem eximi 1833

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

Syntax hints:   → wi 4  ∃wex 1777

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

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

This theorem is referenced by:  2eximi  1834  eximii  1835  exa1  1836  exsimpl  1867  exsimpr  1868  19.29r2  1874  19.29x  1875  19.35  1876  19.40-2  1886  emptyex  1906  exlimiv  1929  speimfwALT  1964  19.12  2331  ax13lem2  2384  exdistrf  2455  equs45f  2467  dfmoeu  2539  moimi  2548  eu6  2577  2eu2ex  2646  reximi2  3085  cgsexg  3536  gencbvex  3553  eqvincg  3661  sbcg  3883  n0rex  4380  axrep2  5306  bm1.3ii  5320  ax6vsep  5321  copsexgw  5510  copsexg  5511  relopabi  5846  dminss  6184  imainss  6185  iotanul2  6543  iotaexOLD  6553  fv3  6938  ssimaex  7007  dffv2  7017  exfo  7139  oprabidw  7479  oprabid  7480  zfrep6  7995  frxp  8167  suppimacnvss  8214  tz7.48-1  8499  enssdom  9037  enfii  9252  fineqvlem  9325  enp1i  9341  infcntss  9390  infeq5  9706  omex  9712  rankuni  9932  scott0  9955  acni3  10116  acnnum  10121  dfac3  10190  dfac9  10206  kmlem1  10220  cflm  10319  cfcof  10343  axdc4lem  10524  axcclem  10526  ac6c4  10550  ac6s  10553  ac6s2  10555  axdclem2  10589  brdom3  10597  brdom5  10598  brdom4  10599  nqpr  11083  ltexprlem4  11108  reclem2pr  11117  hash1to3  14541  trclublem  15044  fnpr2ob  17618  drsdirfi  18375  toprntopon  22952  2ndcsb  23478  fbssint  23867  isfil2  23885  alexsubALTlem3  24078  lpbl  24537  metustfbas  24591  lrrecfr  27994  ex-natded9.26-2  30452  19.9d2rf  32498  rexunirn  32520  f1ocnt  32807  fsumiunle  32833  fmcncfil  33877  esumiun  34058  0elsiga  34078  ddemeas  34200  bnj168  34706  bnj593  34721  bnj607  34892  bnj600  34895  bnj916  34909  fineqvpow  35072  wevgblacfn  35076  lfuhgr3  35087  cusgredgex  35089  loop1cycl  35105  umgr2cycl  35109  fundmpss  35730  exisym1  36390  bj-sylge  36590  bj-19.12  36727  bj-equs45fv  36777  bj-snsetex  36929  bj-snglss  36936  bj-snglex  36939  bj-bm1.3ii  37030  bj-restn0  37056  bj-ccinftydisj  37179  mptsnunlem  37304  pibt2  37383  wl-cbvmotv  37467  wl-moae  37470  wl-nax6im  37472  eu6w  42631  iscard4  43495  ismnushort  44270  spsbce-2  44350  iotaexeu  44387  iotasbc  44388  relopabVD  44872  ax6e2ndeqVD  44880  2uasbanhVD  44882  ax6e2ndeqALT  44902  fnchoice  44929  rfcnnnub  44936  stoweidlem35  45956  stoweidlem57  45978  mo0sn  48547