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  3540  fvmptdv2  7004  fprresex  8309  wfrlem17OLD  8339  tfrlem9a  8400  erref  8739  domdifsn  9068  xpdom2  9081  enfixsn  9095  sucdom2OLD  9096  domunsn  9141  mapdom1  9156  sucdom2  9217  fineqvlem  9270  fissuni  9369  fipreima  9370  indexfi  9372  brwdom2  9587  wdomtr  9589  unwdomg  9598  unxpwdom  9603  infdifsn  9671  isinffi  10006  ac5num  10050  numacn  10063  acndom  10065  acndom2  10068  fodomacn  10070  infpss  10230  ssfin4  10324  domfin4  10325  enfin2i  10335  fin23lem31  10357  fin23lem41  10366  axcclem  10471  canthp1lem1  10666  canthp1  10668  winafp  10711  wun0  10732  prlem936  11061  supmul  12214  supxrre  13343  infxrre  13353  ixxub  13383  ixxlb  13384  hash1elsn  14389  relexpindlem  15082  isumltss  15864  eulerth  16802  ramub2  17034  mrieqv2d  17651  mreexexlem4d  17659  acsinfd  18566  acsdomd  18567  dfgrp3lem  19021  issubg2  19124  psgnunilem3  19477  sylow1lem4  19582  sylow3  19614  prmcyg  19875  ablfaclem3  20070  lbspss  21040  lsmcv  21102  cygzn  21531  lbslcic  21801  lmff  23239  tgcmp  23339  hauscmplem  23344  clsconn  23368  2ndcsep  23397  1stcelcls  23399  ptcnplem  23559  txcn  23564  fbdmn0  23772  ptcmplem2  23991  ptcmplem3  23992  tsmsxplem1  24091  met2ndci  24461  nmoid  24681  phtpcer  24945  phtpcco2  24950  cmetcau  25241  iscmet3lem2  25244  bcthlem4  25279  bcthlem5  25280  ovolicc2lem2  25471  vitali  25566  mbfimaopnlem  25608  limciun  25847  vieta1lem2  26271  tgldim0eq  28482  hpgerlem  28744  cusgrfi  29438  fusgrmaxsize  29444  minvecolem5  30862  n0limd  32453  foresf1o  32485  unidifsnel  32516  unidifsnne  32517  2ndimaxp  32624  aciunf1lem  32640  fsumiunle  32808  gsumwrd2dccatlem  33060  cycpmconjslem2  33166  cycpmconjs  33167  elrspunidl  33443  ssdifidlprm  33473  krullndrng  33496  qsdrng  33512  1arithidom  33552  1arithufdlem4  33562  dimcl  33642  lmimdim  33643  lmicdim  33644  lvecdim0i  33645  lvecdim0  33646  lssdimle  33647  dimpropd  33648  dimkerim  33667  fedgmul  33671  extdg1id  33707  locfinref  33872  esumcst  34094  esumiun  34125  unelldsys  34189  sigapildsys  34193  carsggect  34350  carsgclctunlem3  34352  erdsze2lem1  35225  erdsze2  35227  ptpconn  35255  cvmliftpht  35340  filnetlem3  36398  numiunnum  36488  exlimimd  37361  poimirlem32  37676  mblfinlem2  37682  mblfinlem3  37683  mblfinlem4  37684  sdclem1  37767  sstotbnd  37799  prdsbnd  37817  prdstotbnd  37818  heibor1lem  37833  bfp  37848  eqvrelref  38628  llnn0  39535  lplnn0N  39566  lvoln0N  39610  diaglbN  41074  diaintclN  41077  dibglbN  41185  dibintclN  41186  dihglblem2aN  41312  dihintcl  41363  dvh1dim  41461  sticksstones20  42179  eldioph2lem1  42783  eldioph2lem2  42784  rencldnfilem  42843  kelac1  43087  hbt  43154  cpcoll2d  44283  cncmpmax  45056  lptre2pt  45669  itgsubsticclem  46004  stoweidlem28  46057  stoweidlem31  46060  stoweidlem46  46075  stoweidlem53  46082  stoweidlem59  46088  uniimaelsetpreimafv  47410  iinfssc  49024  iinfsubc  49025  imaid  49094  thincciso4  49343  termcbas2  49367  termchom  49373  termcterm2  49399  euendfunc  49411  termcarweu  49413  diag1f1o  49419  diag2f1o  49422  setrec1  49555