Theorem exlimddv 1968

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  vtocld  3529  n0limd  4308  fvmptdv2  7012  fprresex  8309  tfrlem9a  8375  erref  8717  domdifsn  9051  xpdom2  9063  enfixsn  9077  domunsn  9118  mapdom1  9133  sucdom2  9190  fineqvlem  9229  fissuni  9317  fipreima  9318  indexfi  9320  brwdom2  9538  wdomtr  9540  unwdomg  9549  unxpwdom  9554  infdifsn  9629  isinffi  9990  ac5num  10032  numacn  10045  acndom  10047  acndom2  10050  fodomacn  10052  infpss  10211  ssfin4  10305  domfin4  10306  enfin2i  10316  fin23lem31  10338  fin23lem41  10347  axcclem  10452  canthp1lem1  10648  canthp1  10650  winafp  10693  wun0  10714  prlem936  11043  supmul  12198  supxrre  13364  infxrre  13374  ixxub  13404  ixxlb  13405  hash1elsn  14420  relexpindlem  15119  isumltss  15920  eulerth  16859  ramub2  17091  mrieqv2d  17712  mreexexlem4d  17720  acsinfd  18629  acsdomd  18630  dfgrp3lem  19127  issubg2  19231  psgnunilem3  19589  sylow1lem4  19694  sylow3  19726  prmcyg  19987  ablfaclem3  20182  lbspss  21232  lsmcv  21294  ssdifidlprm  21515  cygzn  21749  lbslcic  22020  lmff  23487  tgcmp  23587  hauscmplem  23592  clsconn  23616  2ndcsep  23645  1stcelcls  23647  ptcnplem  23807  txcn  23812  fbdmn0  24020  ptcmplem2  24239  ptcmplem3  24240  tsmsxplem1  24339  met2ndci  24708  nmoid  24928  phtpcer  25183  phtpcco2  25187  cmetcau  25477  iscmet3lem2  25480  bcthlem4  25515  bcthlem5  25516  ovolicc2lem2  25706  vitali  25801  mbfimaopnlem  25843  limciun  26082  vieta1lem2  26501  tgldim0eq  28801  hpgerlem  29076  cusgrfi  29837  fusgrmaxsize  29843  minvecolem5  31262  foresf1o  32879  unidifsnel  32910  unidifsnne  32911  2ndimaxp  33020  aciunf1lem  33036  padct  33092  fsumiunle  33202  gsumwrd2dccatlem  33420  cycpmconjslem2  33498  cycpmconjs  33499  elrspunidl  33759  krullndrng  33786  qsdrng  33802  dflring3  33810  1arithidom  33850  1arithufdlem4  33860  dimcl  34016  lmimdim  34017  lmicdim  34018  lvecdim0i  34019  lvecdim0  34020  lssdimle  34021  dimpropd  34022  dimkerim  34040  fedgmul  34044  extdg1id  34079  locfinref  34254  esumcst  34476  esumiun  34507  unelldsys  34572  sigapildsys  34576  carsggect  34732  carsgclctunlem3  34734  erdsze2lem1  35708  erdsze2  35710  ptpconn  35738  cvmliftpht  35823  filnetlem3  36924  numiunnum  37014  exlimimd  38022  poimirlem32  38336  mblfinlem2  38342  mblfinlem3  38343  mblfinlem4  38344  sdclem1  38427  sstotbnd  38459  prdsbnd  38477  prdstotbnd  38478  heibor1lem  38493  bfp  38508  eqvrelref  39376  llnn0  40323  lplnn0N  40354  lvoln0N  40398  diaglbN  41862  diaintclN  41865  dibglbN  41973  dibintclN  41974  dihglblem2aN  42100  dihintcl  42151  dvh1dim  42249  sticksstones20  42966  eldioph2lem1  43524  eldioph2lem2  43525  rencldnfilem  43580  kelac1  43823  hbt  43890  cpcoll2d  45002  cncmpmax  45785  lptre2pt  46387  itgsubsticclem  46722  stoweidlem28  46775  stoweidlem31  46778  stoweidlem46  46793  stoweidlem53  46800  stoweidlem59  46806  uniimaelsetpreimafv  48178  iinfssc  49868  iinfsubc  49869  imaid  49965  uobrcl  50004  uobeq2  50212  thincciso4  50268  termcbas2  50293  termchom  50299  termcterm2  50325  euendfunc  50337  termcarweu  50339  diag1f1o  50345  diag2f1o  50348  termfucterm  50355  uobeqterm  50357  setrec1  50502