Theorem exlimddv 1934

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  vtocld  3573  fvmptdv2  7047  fprresex  8351  wfrlem17OLD  8381  tfrlem9a  8442  erref  8783  domdifsn  9120  xpdom2  9133  enfixsn  9147  sucdom2OLD  9148  domunsn  9193  mapdom1  9208  sucdom2  9269  fineqvlem  9325  fissuni  9427  fipreima  9428  indexfi  9430  brwdom2  9642  wdomtr  9644  unwdomg  9653  unxpwdom  9658  infdifsn  9726  isinffi  10061  ac5num  10105  numacn  10118  acndom  10120  acndom2  10123  fodomacn  10125  infpss  10285  ssfin4  10379  domfin4  10380  enfin2i  10390  fin23lem31  10412  fin23lem41  10421  axcclem  10526  canthp1lem1  10721  canthp1  10723  winafp  10766  wun0  10787  prlem936  11116  supmul  12267  supxrre  13389  infxrre  13398  ixxub  13428  ixxlb  13429  hash1elsn  14420  relexpindlem  15112  isumltss  15896  eulerth  16830  ramub2  17061  mrieqv2d  17697  mreexexlem4d  17705  acsinfd  18626  acsdomd  18627  dfgrp3lem  19078  issubg2  19181  psgnunilem3  19538  sylow1lem4  19643  sylow3  19675  prmcyg  19936  ablfaclem3  20131  lbspss  21104  lsmcv  21166  cygzn  21612  lbslcic  21884  lmff  23330  tgcmp  23430  hauscmplem  23435  clsconn  23459  2ndcsep  23488  1stcelcls  23490  ptcnplem  23650  txcn  23655  fbdmn0  23863  ptcmplem2  24082  ptcmplem3  24083  tsmsxplem1  24182  met2ndci  24556  nmoid  24784  phtpcer  25046  phtpcco2  25051  cmetcau  25342  iscmet3lem2  25345  bcthlem4  25380  bcthlem5  25381  ovolicc2lem2  25572  vitali  25667  mbfimaopnlem  25709  limciun  25949  vieta1lem2  26371  tgldim0eq  28529  hpgerlem  28791  cusgrfi  29494  fusgrmaxsize  29500  minvecolem5  30913  n0limd  32501  foresf1o  32532  unidifsnel  32563  unidifsnne  32564  2ndimaxp  32665  aciunf1lem  32680  fsumiunle  32833  cycpmconjslem2  33148  cycpmconjs  33149  elrspunidl  33421  ssdifidlprm  33451  krullndrng  33474  qsdrng  33490  1arithidom  33530  1arithufdlem4  33540  dimcl  33615  lmimdim  33616  lmicdim  33617  lvecdim0i  33618  lvecdim0  33619  lssdimle  33620  dimpropd  33621  dimkerim  33640  fedgmul  33644  extdg1id  33676  locfinref  33787  esumcst  34027  esumiun  34058  unelldsys  34122  sigapildsys  34126  carsggect  34283  carsgclctunlem3  34285  erdsze2lem1  35171  erdsze2  35173  ptpconn  35201  cvmliftpht  35286  filnetlem3  36346  numiunnum  36436  exlimimd  37309  poimirlem32  37612  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  sdclem1  37703  sstotbnd  37735  prdsbnd  37753  prdstotbnd  37754  heibor1lem  37769  bfp  37784  eqvrelref  38566  llnn0  39473  lplnn0N  39504  lvoln0N  39548  diaglbN  41012  diaintclN  41015  dibglbN  41123  dibintclN  41124  dihglblem2aN  41250  dihintcl  41301  dvh1dim  41399  sticksstones20  42123  eldioph2lem1  42716  eldioph2lem2  42717  rencldnfilem  42776  kelac1  43020  hbt  43087  cpcoll2d  44228  cncmpmax  44932  lptre2pt  45561  itgsubsticclem  45896  stoweidlem28  45949  stoweidlem31  45952  stoweidlem46  45967  stoweidlem53  45974  stoweidlem59  45980  uniimaelsetpreimafv  47270  setrec1  48783