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  1910  19.29x  1911  19.35  1912  19.40-2  1922  emptyex  1942  exlimiv  1965  speimfwALT  1999  nfexhe  2214  ax12ev2c  2220  19.12  2361  ax13lem2  2408  exdistrf  2479  equs45f  2491  dfmoeu  2563  eu6  2602  2eu2ex  2671  reximi2  3099  cgsexg  3498  gencbvex  3510  eqvincg  3605  sbcg  3814  n0rex  4308  axrep2  5238  sepex  5258  ax6vsep  5260  axprg  5399  copsexgwOLD  5465  copsexg  5466  relopabiOLD  5806  dmcoss  5964  dminss  6155  imainss  6156  iotanul2  6529  fv3  6926  ssimaex  6993  dffv2  7003  exfo  7129  oprabidw  7474  oprabid  7475  zfrep6OLD  7991  frxp  8165  suppimacnvss  8218  tz7.48-1  8481  enssdom  9031  enssdomOLD  9032  enfii  9229  fineqvlem  9285  enp1i  9298  infcntss  9342  infeq5  9665  rankuni  9906  scott0b  9964  scott0OLD  9965  acni3  10153  acnnum  10158  dfac3  10227  dfac9  10242  kmlem1  10256  cflm  10354  cfcof  10379  axdc4lem  10560  axcclem  10562  ac6c4  10586  ac6s  10589  ac6s2  10591  axdclem2  10625  brdom3  10634  brdom5  10635  brdom4  10636  nqpr  11126  ltexprlem4  11151  reclem2pr  11160  hash1to3  14664  trclublem  15177  fnpr2ob  17759  drsdirfi  18508  toprntopon  23273  2ndcsb  23797  fbssint  24187  isfil2  24205  alexsubALTlem3  24398  lpbl  24852  metustfbas  24906  lrrecfr  28359  lfuhgr3  29758  loop1cycl  30774  umgr2cycl  30777  ex-natded9.26-2  31051  19.9d2rf  33138  rexunirn  33160  f1ocnt  33462  fsumiunle  33490  fmcncfil  34633  esumiun  34796  0elsiga  34816  ddemeas  34939  bnj168  35431  bnj593  35446  bnj607  35616  bnj600  35619  bnj916  35633  abweex  35801  axprALT2  35816  acwer1prclem  35851  fineqvpow  35883  tz9.1regs  35902  kardeq0  35924  onvf1odlem1  36031  wevgblacfn  36039  cusgredgex  36063  ptpconn  36165  mirimanofffr  36629  fundmpss  36710  exisym1  37390  axtco2g  37443  bj-sylge  37684  bj-exextruan  37715  bj-cbvew  37719  bj-19.12  37803  bj-equs45fv  37901  bj-snsetex  38054  bj-snglss  38061  bj-snglex  38064  bj-bm1.3ii  38170  bj-axnul  38179  bj-axseprep  38181  bj-restn0  38202  bj-ccinftydisj  38326  mptsnunlem  38453  pibt2  38532  wl-cbvmotv  38637  wl-moae  38640  wl-nax6im  38642  impprop  38836  eu6w  43880  iscard4  44726  ismnushort  45477  spsbce-2  45557  iotaexeu  45593  iotasbc  45594  relopabVD  46074  ax6e2ndeqVD  46082  2uasbanhVD  46084  ax6e2ndeqALT  46104  fnchoice  46251  rfcnnnub  46258  stoweidlem35  47250  stoweidlem57  47272  mo0sn  50132