Theorem exlimddv 1936

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

Syntax hints:   → wi 4   ∧ wa 399  ∃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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  vtocld  3473  fvmptdv2  6777  wfrlem17  7981  tfrlem9a  8032  erref  8319  domdifsn  8621  xpdom2  8633  enfixsn  8647  sucdom2  8648  domunsn  8689  mapdom1  8704  fineqvlem  8770  fissuni  8862  fipreima  8863  indexfi  8865  brwdom2  9070  wdomtr  9072  unwdomg  9081  unxpwdom  9086  infdifsn  9153  isinffi  9454  ac5num  9496  numacn  9509  acndom  9511  acndom2  9514  fodomacn  9516  infpss  9677  ssfin4  9770  domfin4  9771  enfin2i  9781  fin23lem31  9803  fin23lem41  9812  axcclem  9917  canthp1lem1  10112  canthp1  10114  winafp  10157  wun0  10178  prlem936  10507  supmul  11649  supxrre  12761  infxrre  12770  ixxub  12800  ixxlb  12801  hash1elsn  13782  relexpindlem  14470  isumltss  15251  eulerth  16175  ramub2  16405  mrieqv2d  16968  mreexexlem4d  16976  acsinfd  17856  acsdomd  17857  dfgrp3lem  18264  issubg2  18361  psgnunilem3  18691  sylow1lem4  18793  sylow3  18825  prmcyg  19082  ablfaclem3  19277  lbspss  19922  lsmcv  19981  cygzn  20338  lbslcic  20606  lmff  22001  tgcmp  22101  hauscmplem  22106  clsconn  22130  2ndcsep  22159  1stcelcls  22161  ptcnplem  22321  txcn  22326  fbdmn0  22534  ptcmplem2  22753  ptcmplem3  22754  tsmsxplem1  22853  met2ndci  23224  nmoid  23444  phtpcer  23696  phtpcco2  23700  cmetcau  23989  iscmet3lem2  23992  bcthlem4  24027  bcthlem5  24028  ovolicc2lem2  24218  vitali  24313  mbfimaopnlem  24355  limciun  24593  vieta1lem2  25006  tgldim0eq  26396  hpgerlem  26658  cusgrfi  27347  fusgrmaxsize  27353  minvecolem5  28763  foresf1o  30372  unidifsnel  30405  unidifsnne  30406  2ndimaxp  30507  aciunf1lem  30523  fsumiunle  30667  cycpmconjslem2  30948  cycpmconjs  30949  elrspunidl  31127  dimcl  31209  lvecdim0i  31210  lvecdim0  31211  lssdimle  31212  dimpropd  31213  dimkerim  31229  fedgmul  31233  extdg1id  31259  locfinref  31312  esumcst  31550  esumiun  31581  unelldsys  31645  sigapildsys  31649  carsggect  31804  carsgclctunlem3  31806  erdsze2lem1  32681  erdsze2  32683  ptpconn  32711  cvmliftpht  32796  filnetlem3  34118  exlimimd  35040  poimirlem32  35369  mblfinlem2  35375  mblfinlem3  35376  mblfinlem4  35377  sdclem1  35461  sstotbnd  35493  prdsbnd  35511  prdstotbnd  35512  heibor1lem  35527  bfp  35542  eqvrelref  36285  llnn0  37092  lplnn0N  37123  lvoln0N  37167  diaglbN  38631  diaintclN  38634  dibglbN  38742  dibintclN  38743  dihglblem2aN  38869  dihintcl  38920  dvh1dim  39018  eldioph2lem1  40074  eldioph2lem2  40075  rencldnfilem  40134  kelac1  40380  hbt  40447  cpcoll2d  41340  cncmpmax  42034  lptre2pt  42648  itgsubsticclem  42983  stoweidlem28  43036  stoweidlem31  43039  stoweidlem46  43054  stoweidlem53  43061  stoweidlem59  43067  uniimaelsetpreimafv  44281  setrec1  45612