Theorem exlimddv 1954

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

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799

This theorem is referenced by:  vtocld  3526  fvmptdv2  6989  fprresex  8285  tfrlem9a  8351  erref  8693  domdifsn  9026  xpdom2  9038  enfixsn  9052  domunsn  9093  mapdom1  9108  sucdom2  9165  fineqvlem  9204  fissuni  9294  fipreima  9295  indexfi  9297  brwdom2  9515  wdomtr  9517  unwdomg  9526  unxpwdom  9531  infdifsn  9606  isinffi  9944  ac5num  9986  numacn  9999  acndom  10001  acndom2  10004  fodomacn  10006  infpss  10166  ssfin4  10261  domfin4  10262  enfin2i  10272  fin23lem31  10294  fin23lem41  10303  axcclem  10408  canthp1lem1  10604  canthp1  10606  winafp  10649  wun0  10670  prlem936  10999  supmul  12158  supxrre  13324  infxrre  13334  ixxub  13364  ixxlb  13365  hash1elsn  14378  relexpindlem  15070  isumltss  15869  eulerth  16809  ramub2  17041  mrieqv2d  17662  mreexexlem4d  17670  acsinfd  18579  acsdomd  18580  dfgrp3lem  19071  issubg2  19174  psgnunilem3  19527  sylow1lem4  19632  sylow3  19664  prmcyg  19925  ablfaclem3  20120  lbspss  21137  lsmcv  21199  cygzn  21610  lbslcic  21881  lmff  23349  tgcmp  23449  hauscmplem  23454  clsconn  23478  2ndcsep  23507  1stcelcls  23509  ptcnplem  23669  txcn  23674  fbdmn0  23882  ptcmplem2  24101  ptcmplem3  24102  tsmsxplem1  24201  met2ndci  24570  nmoid  24790  phtpcer  25045  phtpcco2  25049  cmetcau  25339  iscmet3lem2  25342  bcthlem4  25377  bcthlem5  25378  ovolicc2lem2  25568  vitali  25663  mbfimaopnlem  25705  limciun  25944  vieta1lem2  26363  tgldim0eq  28660  hpgerlem  28922  cusgrfi  29616  fusgrmaxsize  29622  minvecolem5  31041  n0limd  32630  foresf1o  32663  unidifsnel  32694  unidifsnne  32695  2ndimaxp  32809  aciunf1lem  32825  padct  32881  fsumiunle  32992  gsumwrd2dccatlem  33218  cycpmconjslem2  33296  cycpmconjs  33297  elrspunidl  33575  ssdifidlprm  33606  krullndrng  33630  qsdrng  33646  dflring3  33654  1arithidom  33694  1arithufdlem4  33704  dimcl  33861  lmimdim  33862  lmicdim  33863  lvecdim0i  33864  lvecdim0  33865  lssdimle  33866  dimpropd  33867  dimkerim  33885  fedgmul  33889  extdg1id  33924  locfinref  34099  esumcst  34321  esumiun  34352  unelldsys  34416  sigapildsys  34420  carsggect  34576  carsgclctunlem3  34578  erdsze2lem1  35514  erdsze2  35516  ptpconn  35544  cvmliftpht  35629  filnetlem3  36701  numiunnum  36791  exlimimd  37798  poimirlem32  38112  mblfinlem2  38118  mblfinlem3  38119  mblfinlem4  38120  sdclem1  38203  sstotbnd  38235  prdsbnd  38253  prdstotbnd  38254  heibor1lem  38269  bfp  38284  eqvrelref  39154  llnn0  40101  lplnn0N  40132  lvoln0N  40176  diaglbN  41640  diaintclN  41643  dibglbN  41751  dibintclN  41752  dihglblem2aN  41878  dihintcl  41929  dvh1dim  42027  sticksstones20  42744  eldioph2lem1  43302  eldioph2lem2  43303  rencldnfilem  43358  kelac1  43601  hbt  43668  cpcoll2d  44796  cncmpmax  45573  lptre2pt  46175  itgsubsticclem  46510  stoweidlem28  46563  stoweidlem31  46566  stoweidlem46  46581  stoweidlem53  46588  stoweidlem59  46594  uniimaelsetpreimafv  47963  iinfssc  49639  iinfsubc  49640  imaid  49736  uobrcl  49775  uobeq2  49983  thincciso4  50039  termcbas2  50064  termchom  50070  termcterm2  50096  euendfunc  50108  termcarweu  50110  diag1f1o  50116  diag2f1o  50119  termfucterm  50126  uobeqterm  50128  setrec1  50273