Theorem exlimddv 1935

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  vtocld  3530  fvmptdv2  6989  fprresex  8292  tfrlem9a  8357  erref  8694  domdifsn  9028  xpdom2  9041  enfixsn  9055  sucdom2OLD  9056  domunsn  9097  mapdom1  9112  sucdom2  9173  fineqvlem  9216  fissuni  9315  fipreima  9316  indexfi  9318  brwdom2  9533  wdomtr  9535  unwdomg  9544  unxpwdom  9549  infdifsn  9617  isinffi  9952  ac5num  9996  numacn  10009  acndom  10011  acndom2  10014  fodomacn  10016  infpss  10176  ssfin4  10270  domfin4  10271  enfin2i  10281  fin23lem31  10303  fin23lem41  10312  axcclem  10417  canthp1lem1  10612  canthp1  10614  winafp  10657  wun0  10678  prlem936  11007  supmul  12162  supxrre  13294  infxrre  13304  ixxub  13334  ixxlb  13335  hash1elsn  14343  relexpindlem  15036  isumltss  15821  eulerth  16760  ramub2  16992  mrieqv2d  17607  mreexexlem4d  17615  acsinfd  18522  acsdomd  18523  dfgrp3lem  18977  issubg2  19080  psgnunilem3  19433  sylow1lem4  19538  sylow3  19570  prmcyg  19831  ablfaclem3  20026  lbspss  20996  lsmcv  21058  cygzn  21487  lbslcic  21757  lmff  23195  tgcmp  23295  hauscmplem  23300  clsconn  23324  2ndcsep  23353  1stcelcls  23355  ptcnplem  23515  txcn  23520  fbdmn0  23728  ptcmplem2  23947  ptcmplem3  23948  tsmsxplem1  24047  met2ndci  24417  nmoid  24637  phtpcer  24901  phtpcco2  24906  cmetcau  25196  iscmet3lem2  25199  bcthlem4  25234  bcthlem5  25235  ovolicc2lem2  25426  vitali  25521  mbfimaopnlem  25563  limciun  25802  vieta1lem2  26226  tgldim0eq  28437  hpgerlem  28699  cusgrfi  29393  fusgrmaxsize  29399  minvecolem5  30817  n0limd  32408  foresf1o  32440  unidifsnel  32471  unidifsnne  32472  2ndimaxp  32577  aciunf1lem  32593  fsumiunle  32761  gsumwrd2dccatlem  33013  cycpmconjslem2  33119  cycpmconjs  33120  elrspunidl  33406  ssdifidlprm  33436  krullndrng  33459  qsdrng  33475  1arithidom  33515  1arithufdlem4  33525  dimcl  33605  lmimdim  33606  lmicdim  33607  lvecdim0i  33608  lvecdim0  33609  lssdimle  33610  dimpropd  33611  dimkerim  33630  fedgmul  33634  extdg1id  33668  locfinref  33838  esumcst  34060  esumiun  34091  unelldsys  34155  sigapildsys  34159  carsggect  34316  carsgclctunlem3  34318  erdsze2lem1  35197  erdsze2  35199  ptpconn  35227  cvmliftpht  35312  filnetlem3  36375  numiunnum  36465  exlimimd  37338  poimirlem32  37653  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  sdclem1  37744  sstotbnd  37776  prdsbnd  37794  prdstotbnd  37795  heibor1lem  37810  bfp  37825  eqvrelref  38608  llnn0  39517  lplnn0N  39548  lvoln0N  39592  diaglbN  41056  diaintclN  41059  dibglbN  41167  dibintclN  41168  dihglblem2aN  41294  dihintcl  41345  dvh1dim  41443  sticksstones20  42161  eldioph2lem1  42755  eldioph2lem2  42756  rencldnfilem  42815  kelac1  43059  hbt  43126  cpcoll2d  44255  cncmpmax  45033  lptre2pt  45645  itgsubsticclem  45980  stoweidlem28  46033  stoweidlem31  46036  stoweidlem46  46051  stoweidlem53  46058  stoweidlem59  46064  uniimaelsetpreimafv  47401  iinfssc  49050  iinfsubc  49051  imaid  49147  uobrcl  49186  uobeq2  49394  thincciso4  49450  termcbas2  49475  termchom  49481  termcterm2  49507  euendfunc  49519  termcarweu  49521  diag1f1o  49527  diag2f1o  49530  termfucterm  49537  uobeqterm  49539  setrec1  49684