Theorem eximi 1837

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

Syntax hints:   → wi 4  ∃wex 1781

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

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

This theorem is referenced by:  2eximi  1838  eximii  1839  exa1  1840  exsimpl  1870  exsimpr  1871  19.29r2  1877  19.29x  1878  19.35  1879  19.40-2  1889  emptyex  1909  exlimiv  1932  speimfwALT  1966  nfexhe  2183  19.12  2332  ax13lem2  2380  exdistrf  2451  equs45f  2463  dfmoeu  2535  eu6  2574  2eu2ex  2643  reximi2  3070  cgsexg  3474  gencbvex  3487  eqvincg  3590  sbcg  3801  n0rex  4297  axrep2  5215  sepex  5235  bm1.3iiOLD  5237  ax6vsep  5238  axprg  5379  copsexgwOLD  5444  copsexg  5445  relopabi  5778  dmcoss  5930  dminss  6117  imainss  6118  iotanul2  6471  fv3  6858  ssimaex  6925  dffv2  6935  exfo  7057  oprabidw  7398  oprabid  7399  zfrep6OLD  7908  frxp  8076  suppimacnvss  8123  tz7.48-1  8382  enssdom  8923  enssdomOLD  8924  enfii  9120  fineqvlem  9176  enp1i  9189  infcntss  9233  infeq5  9558  rankuni  9787  scott0  9810  acni3  9969  acnnum  9974  dfac3  10043  dfac9  10059  kmlem1  10073  cflm  10172  cfcof  10196  axdc4lem  10377  axcclem  10379  ac6c4  10403  ac6s  10406  ac6s2  10408  axdclem2  10442  brdom3  10450  brdom5  10451  brdom4  10452  nqpr  10937  ltexprlem4  10962  reclem2pr  10971  hash1to3  14454  trclublem  14957  fnpr2ob  17522  drsdirfi  18271  toprntopon  22890  2ndcsb  23414  fbssint  23803  isfil2  23821  alexsubALTlem3  24014  lpbl  24468  metustfbas  24522  lrrecfr  27935  ex-natded9.26-2  30490  19.9d2rf  32538  rexunirn  32561  f1ocnt  32873  fsumiunle  32902  fmcncfil  34075  esumiun  34238  0elsiga  34258  ddemeas  34380  bnj168  34873  bnj593  34888  bnj607  35058  bnj600  35061  bnj916  35075  axprALT2  35253  fineqvpow  35259  tz9.1regs  35278  onvf1odlem1  35285  wevgblacfn  35291  lfuhgr3  35302  cusgredgex  35304  loop1cycl  35319  umgr2cycl  35323  fundmpss  35949  exisym1  36606  axtco2g  36659  bj-sylge  36901  bj-exextruan  36932  bj-cbvew  36936  bj-19.12  37020  bj-equs45fv  37118  bj-snsetex  37270  bj-snglss  37277  bj-snglex  37280  bj-bm1.3ii  37371  bj-axnul  37379  bj-axseprep  37381  bj-restn0  37402  bj-ccinftydisj  37527  mptsnunlem  37654  pibt2  37733  wl-cbvmotv  37838  wl-moae  37841  wl-nax6im  37843  eu6w  43109  iscard4  43960  ismnushort  44728  spsbce-2  44808  iotaexeu  44845  iotasbc  44846  relopabVD  45327  ax6e2ndeqVD  45335  2uasbanhVD  45337  ax6e2ndeqALT  45357  fnchoice  45460  rfcnnnub  45467  stoweidlem35  46463  stoweidlem57  46485  mo0sn  49291