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  3522  n0limd  4301  fvmptdv2  7005  fprresex  8309  tfrlem9a  8375  erref  8717  domdifsn  9058  xpdom2  9070  enfixsn  9084  domunsn  9125  mapdom1  9140  sucdom2  9197  fineqvlem  9236  fissuni  9324  fipreima  9325  indexfi  9327  brwdom2  9545  wdomtr  9547  unwdomg  9556  unxpwdom  9561  infdifsn  9636  isinffi  9997  ac5num  10039  numacn  10052  acndom  10054  acndom2  10057  fodomacn  10059  infpss  10218  ssfin4  10312  domfin4  10313  enfin2i  10323  fin23lem31  10345  fin23lem41  10354  axcclem  10459  canthp1lem1  10661  canthp1  10663  winafp  10706  wun0  10727  prlem936  11056  supmul  12211  supxrre  13379  infxrre  13389  ixxub  13419  ixxlb  13420  hash1elsn  14435  relexpindlem  15136  isumltss  15937  eulerth  16874  ramub2  17106  mrieqv2d  17727  mreexexlem4d  17735  acsinfd  18644  acsdomd  18645  dfgrp3lem  19161  issubg2  19265  psgnunilem3  19623  sylow1lem4  19728  sylow3  19760  prmcyg  20021  ablfaclem3  20216  lbspss  21266  lsmcv  21328  ssdifidlprm  21549  cygzn  21783  lbslcic  22054  lmff  23526  tgcmp  23626  hauscmplem  23631  clsconn  23655  2ndcsep  23685  1stcelcls  23687  ptcnplem  23847  txcn  23852  fbdmn0  24060  ptcmplem2  24279  ptcmplem3  24280  tsmsxplem1  24379  met2ndci  24748  nmoid  24968  phtpcer  25223  phtpcco2  25227  cmetcau  25517  iscmet3lem2  25520  bcthlem4  25555  bcthlem5  25556  ovolicc2lem2  25746  vitali  25841  mbfimaopnlem  25883  limciun  26121  vieta1lem2  26543  tgldim0eq  28845  hpgerlem  29122  cusgrfi  29918  fusgrmaxsize  29924  minvecolem5  31362  foresf1o  32979  unidifsnel  33010  unidifsnne  33011  2ndimaxp  33119  aciunf1lem  33135  padct  33189  fsumiunle  33299  gsumwrd2dccatlem  33517  cycpmconjslem2  33595  cycpmconjs  33596  elrspunidl  33856  krullndrng  33883  qsdrng  33899  dflring3  33907  1arithidom  33947  1arithufdlem4  33957  dimcl  34113  lmimdim  34114  lmicdim  34115  lvecdim0i  34116  lvecdim0  34117  lssdimle  34118  dimpropd  34119  dimkerim  34137  fedgmul  34141  extdg1id  34176  locfinref  34351  esumcst  34573  esumiun  34604  unelldsys  34669  sigapildsys  34673  carsggect  34829  carsgclctunlem3  34831  erdsze2lem1  35782  erdsze2  35784  ptpconn  35812  cvmliftpht  35897  filnetlem3  36999  numiunnum  37089  exlimimd  38097  poimirlem32  38401  mblfinlem2  38407  mblfinlem3  38408  mblfinlem4  38409  sdclem1  38493  sstotbnd  38525  prdsbnd  38543  prdstotbnd  38544  heibor1lem  38559  bfp  38574  eqvrelref  39442  llnn0  40389  lplnn0N  40420  lvoln0N  40464  diaglbN  41928  diaintclN  41931  dibglbN  42039  dibintclN  42040  dihglblem2aN  42166  dihintcl  42217  dvh1dim  42315  sticksstones20  43032  eldioph2lem1  43605  eldioph2lem2  43606  rencldnfilem  43661  kelac1  43904  hbt  43971  cpcoll2d  45083  cncmpmax  45866  lptre2pt  46468  itgsubsticclem  46803  stoweidlem28  46856  stoweidlem31  46859  stoweidlem46  46874  stoweidlem53  46881  stoweidlem59  46887  tmachlem-franscan  47777  uniimaelsetpreimafv  48296  iinfssc  49983  iinfsubc  49984  imaid  50080  uobrcl  50119  uobeq2  50327  thincciso4  50383  termcbas2  50408  termchom  50414  termcterm2  50440  euendfunc  50452  termcarweu  50454  diag1f1o  50460  diag2f1o  50463  termfucterm  50470  uobeqterm  50472  setrec1  50617