Theorem exlimddv 1863

Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
exlimddv.1	⊢ (𝜑 → ∃𝑥𝜓)
exlimddv.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
exlimddv	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimddv

Step	Hyp	Ref	Expression
1		exlimddv.1	. 2 ⊢ (𝜑 → ∃𝑥𝜓)
2		exlimddv.2	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	2	ex 450	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	3	exlimdv 1861	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 384  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  fvmptdv2  6298  wfrlem17  7431  tfrlem9a  7482  erref  7762  domdifsn  8043  xpdom2  8055  enfixsn  8069  domunsn  8110  mapdom1  8125  sucdom2  8156  fineqvlem  8174  fissuni  8271  fipreima  8272  indexfi  8274  brwdom2  8478  wdomtr  8480  unwdomg  8489  unxpwdom  8494  infdifsn  8554  isinffi  8818  ac5num  8859  numacn  8872  acndom  8874  acndom2  8877  fodomacn  8879  infpss  9039  ssfin4  9132  domfin4  9133  enfin2i  9143  fin23lem31  9165  fin23lem41  9174  axcclem  9279  canthp1lem1  9474  canthp1  9476  winafp  9519  wun0  9540  prlem936  9869  supmul  10995  supxrre  12157  infxrre  12166  ixxub  12196  ixxlb  12197  relexpindlem  13803  isumltss  14580  eulerth  15488  ramub2  15718  mrieqv2d  16299  mreexexlem4d  16307  acsinfd  17180  acsdomd  17181  dfgrp3lem  17513  issubg2  17609  psgnunilem3  17916  sylow1lem4  18016  sylow3  18048  prmcyg  18295  ablfaclem3  18486  lbspss  19082  lsmcv  19141  cygzn  19919  lbslcic  20180  lmff  21105  tgcmp  21204  hauscmplem  21209  clsconn  21233  2ndcsep  21262  1stcelcls  21264  ptcnplem  21424  txcn  21429  fbdmn0  21638  ptcmplem2  21857  ptcmplem3  21858  tsmsxplem1  21956  met2ndci  22327  nmoid  22546  phtpcer  22794  phtpcerOLD  22795  phtpcco2  22799  cmetcau  23087  iscmet3lem2  23090  bcthlem4  23124  bcthlem5  23125  ovolicc2lem2  23286  vitali  23382  mbfimaopnlem  23422  limciun  23658  vieta1lem2  24066  tgldim0eq  25398  hpgerlem  25657  cusgrfi  26354  fusgrmaxsize  26360  minvecolem5  27737  foresf1o  29343  aciunf1lem  29462  fsumiunle  29575  locfinref  29908  esumcst  30125  esumiun  30156  unelldsys  30221  sigapildsys  30225  carsggect  30380  carsgclctunlem3  30382  erdsze2lem1  31185  erdsze2  31187  ptpconn  31215  cvmliftpht  31300  filnetlem3  32375  exlimimd  33190  poimirlem32  33441  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  sdclem1  33539  sstotbnd  33574  prdsbnd  33592  prdstotbnd  33593  heibor1lem  33608  bfp  33623  llnn0  34802  lplnn0N  34833  lvoln0N  34877  diaglbN  36344  diaintclN  36347  dibglbN  36455  dibintclN  36456  dihglblem2aN  36582  dihintcl  36633  dvh1dim  36731  eldioph2lem1  37323  eldioph2lem2  37324  rencldnfilem  37384  kelac1  37633  hbt  37700  cncmpmax  39191  lptre2pt  39872  itgsubsticclem  40191  stoweidlem28  40245  stoweidlem31  40248  stoweidlem46  40263  stoweidlem53  40270  stoweidlem59  40276  setrec1  42438