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  3506  fvmptdv2  6966  fprresex  8260  tfrlem9a  8325  erref  8664  domdifsn  8998  xpdom2  9010  enfixsn  9024  domunsn  9065  mapdom1  9080  sucdom2  9137  fineqvlem  9176  fissuni  9267  fipreima  9268  indexfi  9270  brwdom2  9488  wdomtr  9490  unwdomg  9499  unxpwdom  9504  infdifsn  9578  isinffi  9916  ac5num  9958  numacn  9971  acndom  9973  acndom2  9976  fodomacn  9978  infpss  10138  ssfin4  10232  domfin4  10233  enfin2i  10243  fin23lem31  10265  fin23lem41  10274  axcclem  10379  canthp1lem1  10575  canthp1  10577  winafp  10620  wun0  10641  prlem936  10970  supmul  12128  supxrre  13279  infxrre  13289  ixxub  13319  ixxlb  13320  hash1elsn  14333  relexpindlem  15025  isumltss  15813  eulerth  16753  ramub2  16985  mrieqv2d  17605  mreexexlem4d  17613  acsinfd  18522  acsdomd  18523  dfgrp3lem  19014  issubg2  19117  psgnunilem3  19471  sylow1lem4  19576  sylow3  19608  prmcyg  19869  ablfaclem3  20064  lbspss  21077  lsmcv  21139  cygzn  21550  lbslcic  21821  lmff  23266  tgcmp  23366  hauscmplem  23371  clsconn  23395  2ndcsep  23424  1stcelcls  23426  ptcnplem  23586  txcn  23591  fbdmn0  23799  ptcmplem2  24018  ptcmplem3  24019  tsmsxplem1  24118  met2ndci  24487  nmoid  24707  phtpcer  24962  phtpcco2  24966  cmetcau  25256  iscmet3lem2  25259  bcthlem4  25294  bcthlem5  25295  ovolicc2lem2  25485  vitali  25580  mbfimaopnlem  25622  limciun  25861  vieta1lem2  26277  tgldim0eq  28571  hpgerlem  28833  cusgrfi  29527  fusgrmaxsize  29533  minvecolem5  30952  n0limd  32541  foresf1o  32574  unidifsnel  32605  unidifsnne  32606  2ndimaxp  32719  aciunf1lem  32735  padct  32791  fsumiunle  32902  gsumwrd2dccatlem  33138  cycpmconjslem2  33216  cycpmconjs  33217  elrspunidl  33488  ssdifidlprm  33518  krullndrng  33541  qsdrng  33557  1arithidom  33597  1arithufdlem4  33607  dimcl  33747  lmimdim  33748  lmicdim  33749  lvecdim0i  33750  lvecdim0  33751  lssdimle  33752  dimpropd  33753  dimkerim  33771  fedgmul  33775  extdg1id  33810  locfinref  33985  esumcst  34207  esumiun  34238  unelldsys  34302  sigapildsys  34306  carsggect  34462  carsgclctunlem3  34464  erdsze2lem1  35385  erdsze2  35387  ptpconn  35415  cvmliftpht  35500  filnetlem3  36562  numiunnum  36652  exlimimd  37659  poimirlem32  37973  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  sdclem1  38064  sstotbnd  38096  prdsbnd  38114  prdstotbnd  38115  heibor1lem  38130  bfp  38145  eqvrelref  39015  llnn0  39962  lplnn0N  39993  lvoln0N  40037  diaglbN  41501  diaintclN  41504  dibglbN  41612  dibintclN  41613  dihglblem2aN  41739  dihintcl  41790  dvh1dim  41888  sticksstones20  42605  eldioph2lem1  43192  eldioph2lem2  43193  rencldnfilem  43248  kelac1  43491  hbt  43558  cpcoll2d  44686  cncmpmax  45463  lptre2pt  46068  itgsubsticclem  46403  stoweidlem28  46456  stoweidlem31  46459  stoweidlem46  46474  stoweidlem53  46481  stoweidlem59  46487  uniimaelsetpreimafv  47856  iinfssc  49532  iinfsubc  49533  imaid  49629  uobrcl  49668  uobeq2  49876  thincciso4  49932  termcbas2  49957  termchom  49963  termcterm2  49989  euendfunc  50001  termcarweu  50003  diag1f1o  50009  diag2f1o  50012  termfucterm  50019  uobeqterm  50021  setrec1  50166