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  3523  n0limd  4301  fvmptdv2  7010  fprresex  8321  tfrlem9a  8387  erref  8731  domdifsn  9072  xpdom2  9084  enfixsn  9098  domunsn  9139  mapdom1  9154  sucdom2  9211  fineqvlem  9250  fissuni  9339  fipreima  9340  indexfi  9342  brwdom2  9560  wdomtr  9562  unwdomg  9571  unxpwdom  9576  infdifsn  9651  setrec1  9965  isinffi  10066  ac5num  10108  numacn  10121  acndom  10123  acndom2  10126  fodomacn  10128  infpss  10287  ssfin4  10381  domfin4  10382  enfin2i  10392  fin23lem31  10414  fin23lem41  10423  axcclem  10528  canthp1lem1  10730  canthp1  10732  winafp  10775  wun0  10796  prlem936  11125  supmul  12282  supxrre  13450  infxrre  13460  ixxub  13490  ixxlb  13491  hash1elsn  14508  relexpindlem  15209  isumltss  16010  eulerth  16953  ramub2  17185  mrieqv2d  17806  mreexexlem4d  17814  acsinfd  18723  acsdomd  18724  dfgrp3lem  19241  issubg2  19345  psgnunilem3  19703  sylow1lem4  19808  sylow3  19840  prmcyg  20101  ablfaclem3  20296  lbspss  21350  lsmcv  21412  ssdifidlprm  21635  cygzn  21869  lbslcic  22140  lmff  23612  tgcmp  23712  hauscmplem  23717  clsconn  23741  2ndcsep  23771  1stcelcls  23773  ptcnplem  23933  txcn  23938  fbdmn0  24146  ptcmplem2  24365  ptcmplem3  24366  tsmsxplem1  24465  met2ndci  24834  nmoid  25054  phtpcer  25309  phtpcco2  25313  cmetcau  25603  iscmet3lem2  25606  bcthlem4  25641  bcthlem5  25642  ovolicc2lem2  25832  vitali  25927  mbfimaopnlem  25969  limciun  26207  vieta1lem2  26627  tgldim0eq  28959  hpgerlem  29236  cusgrfi  30032  fusgrmaxsize  30038  minvecolem5  31476  foresf1o  33093  unidifsnel  33124  unidifsnne  33125  2ndimaxp  33233  aciunf1lem  33249  padct  33303  fsumiunle  33413  gsumwrd2dccatlem  33631  cycpmconjslem2  33709  cycpmconjs  33710  elrspunidl  33971  krullndrng  33998  qsdrng  34014  dflring3  34022  1arithidom  34062  1arithufdlem4  34072  dimcl  34228  lmimdim  34229  lmicdim  34230  lvecdim0i  34231  lvecdim0  34232  lssdimle  34233  dimpropd  34234  dimkerim  34252  fedgmul  34256  extdg1id  34291  locfinref  34466  esumcst  34688  esumiun  34719  unelldsys  34784  sigapildsys  34788  carsggect  34943  carsgclctunlem3  34945  erdsze2lem1  35947  erdsze2  35949  ptpconn  35977  cvmliftpht  36062  filnetlem3  37148  numiunnum  37238  exlimimd  38246  poimirlem32  38550  mblfinlem2  38556  mblfinlem3  38557  mblfinlem4  38558  sdclem1  38657  sstotbnd  38689  prdsbnd  38707  prdstotbnd  38708  heibor1lem  38723  bfp  38738  eqvrelref  39606  llnn0  40553  lplnn0N  40584  lvoln0N  40628  diaglbN  42092  diaintclN  42095  dibglbN  42203  dibintclN  42204  dihglblem2aN  42330  dihintcl  42381  dvh1dim  42479  sticksstones20  43196  eldioph2lem1  43750  eldioph2lem2  43751  rencldnfilem  43806  kelac1  44049  hbt  44116  cpcoll2d  45228  cncmpmax  46018  lptre2pt  46619  itgsubsticclem  46954  stoweidlem28  47007  stoweidlem31  47010  stoweidlem46  47025  stoweidlem53  47032  stoweidlem59  47038  tmachlem-franscan  47928  uniimaelsetpreimafv  48447  iinfssc  50134  iinfsubc  50135  imaid  50231  uobrcl  50270  uobeq2  50478  thincciso4  50534  termcbas2  50559  termchom  50565  termcterm2  50591  euendfunc  50603  termcarweu  50605  diag1f1o  50611  diag2f1o  50614  termfucterm  50621  uobeqterm  50623