Theorem exlimddv 1937

Description: Existential elimination rule of natural deduction (Rule C, explained in exlimiv 1932). (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 412	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	3	exlimdv 1935	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395  ∃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  ax-5 1912

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

This theorem is referenced by:  vtocld  3507  fvmptdv2  6960  fprresex  8253  tfrlem9a  8318  erref  8657  domdifsn  8991  xpdom2  9003  enfixsn  9017  domunsn  9058  mapdom1  9073  sucdom2  9130  fineqvlem  9169  fissuni  9260  fipreima  9261  indexfi  9263  brwdom2  9481  wdomtr  9483  unwdomg  9492  unxpwdom  9497  infdifsn  9569  isinffi  9907  ac5num  9949  numacn  9962  acndom  9964  acndom2  9967  fodomacn  9969  infpss  10129  ssfin4  10223  domfin4  10224  enfin2i  10234  fin23lem31  10256  fin23lem41  10265  axcclem  10370  canthp1lem1  10566  canthp1  10568  winafp  10611  wun0  10632  prlem936  10961  supmul  12119  supxrre  13270  infxrre  13280  ixxub  13310  ixxlb  13311  hash1elsn  14324  relexpindlem  15016  isumltss  15804  eulerth  16744  ramub2  16976  mrieqv2d  17596  mreexexlem4d  17604  acsinfd  18513  acsdomd  18514  dfgrp3lem  19005  issubg2  19108  psgnunilem3  19462  sylow1lem4  19567  sylow3  19599  prmcyg  19860  ablfaclem3  20055  lbspss  21069  lsmcv  21131  cygzn  21560  lbslcic  21831  lmff  23276  tgcmp  23376  hauscmplem  23381  clsconn  23405  2ndcsep  23434  1stcelcls  23436  ptcnplem  23596  txcn  23601  fbdmn0  23809  ptcmplem2  24028  ptcmplem3  24029  tsmsxplem1  24128  met2ndci  24497  nmoid  24717  phtpcer  24972  phtpcco2  24976  cmetcau  25266  iscmet3lem2  25269  bcthlem4  25304  bcthlem5  25305  ovolicc2lem2  25495  vitali  25590  mbfimaopnlem  25632  limciun  25871  vieta1lem2  26288  tgldim0eq  28585  hpgerlem  28847  cusgrfi  29542  fusgrmaxsize  29548  minvecolem5  30967  n0limd  32556  foresf1o  32589  unidifsnel  32620  unidifsnne  32621  2ndimaxp  32734  aciunf1lem  32750  padct  32806  fsumiunle  32917  gsumwrd2dccatlem  33153  cycpmconjslem2  33231  cycpmconjs  33232  elrspunidl  33503  ssdifidlprm  33533  krullndrng  33556  qsdrng  33572  1arithidom  33612  1arithufdlem4  33622  dimcl  33762  lmimdim  33763  lmicdim  33764  lvecdim0i  33765  lvecdim0  33766  lssdimle  33767  dimpropd  33768  dimkerim  33787  fedgmul  33791  extdg1id  33826  locfinref  34001  esumcst  34223  esumiun  34254  unelldsys  34318  sigapildsys  34322  carsggect  34478  carsgclctunlem3  34480  erdsze2lem1  35401  erdsze2  35403  ptpconn  35431  cvmliftpht  35516  filnetlem3  36578  numiunnum  36668  exlimimd  37673  poimirlem32  37987  mblfinlem2  37993  mblfinlem3  37994  mblfinlem4  37995  sdclem1  38078  sstotbnd  38110  prdsbnd  38128  prdstotbnd  38129  heibor1lem  38144  bfp  38159  eqvrelref  39029  llnn0  39976  lplnn0N  40007  lvoln0N  40051  diaglbN  41515  diaintclN  41518  dibglbN  41626  dibintclN  41627  dihglblem2aN  41753  dihintcl  41804  dvh1dim  41902  sticksstones20  42619  eldioph2lem1  43206  eldioph2lem2  43207  rencldnfilem  43266  kelac1  43509  hbt  43576  cpcoll2d  44704  cncmpmax  45481  lptre2pt  46086  itgsubsticclem  46421  stoweidlem28  46474  stoweidlem31  46477  stoweidlem46  46492  stoweidlem53  46499  stoweidlem59  46505  uniimaelsetpreimafv  47868  iinfssc  49544  iinfsubc  49545  imaid  49641  uobrcl  49680  uobeq2  49888  thincciso4  49944  termcbas2  49969  termchom  49975  termcterm2  50001  euendfunc  50013  termcarweu  50015  diag1f1o  50021  diag2f1o  50024  termfucterm  50031  uobeqterm  50033  setrec1  50178