Theorem eximi 1868

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  2eximi  1869  eximii  1870  exa1  1871  exsimpl  1901  exsimpr  1902  19.29r2  1908  19.29x  1909  19.35  1910  19.40-2  1920  emptyex  1940  exlimiv  1963  speimfwALT  1997  nfexhe  2211  ax12ev2c  2217  19.12  2358  ax13lem2  2406  exdistrf  2477  equs45f  2489  dfmoeu  2561  eu6  2600  2eu2ex  2669  reximi2  3096  cgsexg  3495  gencbvex  3507  eqvincg  3602  sbcg  3811  n0rex  4305  axrep2  5235  sepex  5255  ax6vsep  5257  axprg  5395  copsexgwOLD  5461  copsexg  5462  relopabi  5800  dmcoss  5957  dminss  6142  imainss  6143  iotanul2  6504  fv3  6895  ssimaex  6962  dffv2  6972  exfo  7097  oprabidw  7443  oprabid  7444  zfrep6OLD  7956  frxp  8127  suppimacnvss  8174  tz7.48-1  8437  enssdom  8987  enssdomOLD  8988  enfii  9185  fineqvlem  9241  enp1i  9254  infcntss  9298  infeq5  9622  rankuni  9860  scott0b  9918  scott0OLD  9919  acni3  10107  acnnum  10112  dfac3  10181  dfac9  10196  kmlem1  10210  cflm  10308  cfcof  10333  axdc4lem  10514  axcclem  10516  ac6c4  10540  ac6s  10543  ac6s2  10545  axdclem2  10579  brdom3  10588  brdom5  10589  brdom4  10590  nqpr  11080  ltexprlem4  11105  reclem2pr  11114  hash1to3  14617  trclublem  15128  fnpr2ob  17710  drsdirfi  18459  toprntopon  23223  2ndcsb  23747  fbssint  24137  isfil2  24155  alexsubALTlem3  24348  lpbl  24802  metustfbas  24856  lrrecfr  28311  lfuhgr3  29710  loop1cycl  30726  umgr2cycl  30729  ex-natded9.26-2  31003  19.9d2rf  33048  rexunirn  33070  f1ocnt  33374  fsumiunle  33402  fmcncfil  34545  esumiun  34708  0elsiga  34728  ddemeas  34851  bnj168  35344  bnj593  35359  bnj607  35529  bnj600  35532  bnj916  35546  axprALT2  35713  fineqvpow  35756  tz9.1regs  35775  kardeq0  35797  onvf1odlem1  35855  wevgblacfn  35863  cusgredgex  35875  fundmpss  36501  exisym1  37182  axtco2g  37235  bj-sylge  37476  bj-exextruan  37507  bj-cbvew  37511  bj-19.12  37595  bj-equs45fv  37693  bj-snsetex  37846  bj-snglss  37853  bj-snglex  37856  bj-bm1.3ii  37947  bj-axnul  37956  bj-axseprep  37958  bj-restn0  37979  bj-ccinftydisj  38102  mptsnunlem  38229  pibt2  38308  wl-cbvmotv  38413  wl-moae  38416  wl-nax6im  38418  impprop  38612  eu6w  43641  iscard4  44492  ismnushort  45244  spsbce-2  45324  iotaexeu  45361  iotasbc  45362  relopabVD  45842  ax6e2ndeqVD  45850  2uasbanhVD  45852  ax6e2ndeqALT  45872  fnchoice  45989  rfcnnnub  45996  stoweidlem35  46989  stoweidlem57  47011  mo0sn  49870