Theorem simprlr 778

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprlr	⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

Proof of Theorem simprlr

Step	Hyp	Ref	Expression
1		simpr 483	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrl 726	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 395

This theorem is referenced by:  fcof1  7302  fliftfun  7326  fprresex  8322  wfrlem17OLD  8352  domunfican  9352  finsschain  9391  suppeqfsuppbi  9410  fsuppunbi  9420  wemapsolem  9581  wemapso  9582  wemapso2lem  9583  cantnf  9724  enfin2i  10352  ttukeylem7  10546  fpwwe2lem2  10663  fpwwe2lem8  10669  fpwwe2lem11  10672  fpwwelem  10676  distrlem4pr  11057  mulcmpblnr  11102  prsrlem1  11103  addsrmo  11104  mulsrmo  11105  divdivdiv  11953  divsubdiv  11968  lediv12a  12145  xmullem  13283  xlemul1a  13307  seqcaopr  14044  leexp2r  14178  hashf1lem1  14455  hashf1lem1OLD  14456  hashf1lem2  14457  fi1uzind  14498  brfi1indALT  14501  wrd2ind  14713  swrdccat  14725  cshweqrep  14811  rtrclreclem4  15048  summolem2  15702  summo  15703  prodmolem2  15919  prodmo  15920  bezoutlem3  16524  bezoutlem4  16525  qredeu  16636  pcadd  16865  vdwlem9  16965  vdwlem10  16966  ramub1lem2  17003  ramub1  17004  cofucl  17881  setcmon  18083  poslubmo  18410  posglbmo  18411  grprcan  18937  isnsg3  19122  ghmpreima  19199  gaorber  19266  psgneu  19468  odcau  19566  lsmsubm  19615  lsmmod  19637  efgsfo  19701  ablfaclem3  20051  rngpropd  20121  ringpropd  20231  islmodd  20756  lmodprop2d  20814  lss1d  20854  lindff1  21761  islindf4  21779  assamulgscmlem2  21840  mplcoe1  21982  mplcoe5  21985  evlslem1  22035  mdetunilem7  22540  mdetunilem8  22541  mdetunilem9  22542  mdetuni0  22543  mdetmul  22545  ppttop  22930  epttop  22932  cnhaus  23278  isreg2  23301  cncmp  23316  1stcfb  23369  2ndcomap  23382  cldllycmp  23419  txcls  23528  ptclsg  23539  ptcnp  23546  txdis1cn  23559  txlly  23560  txnlly  23561  pthaus  23562  txhaus  23571  txkgen  23576  xkohaus  23577  xkococnlem  23583  xkococn  23584  fgabs  23803  rnelfm  23877  hausflimi  23904  hausflim  23905  alexsubALTlem2  23972  alexsubALTlem4  23974  alexsubALT  23975  tgpconncomp  24037  qustgplem  24045  metequiv2  24439  met2ndci  24451  nrmmetd  24503  nlmvscnlem1  24623  reconn  24764  xrge0tsms  24770  ipcnlem1  25193  minveclem3  25377  pmltpc  25399  ovolicc2lem5  25470  ovolicc2  25471  uniioombllem6  25537  dyadmbllem  25548  vitalilem3  25559  mbfmullem  25675  itg2split  25699  itg2mono  25703  bddiblnc  25791  dvlip2  25948  lhop1  25967  dvcnvrelem1  25970  ftc1lem6  25996  itgsubst  26004  dgrco  26230  plyexmo  26268  ulmdvlem3  26358  abelthlem2  26389  abelthlem8  26396  mpodvdsmulf1o  27146  dvdsmulf1o  27148  chpchtsum  27172  dchrptlem2  27218  2sqlem5  27375  2sqlem9  27380  2sqb  27385  pntrlog2bnd  27537  pntibndlem3  27545  pntlemp  27563  pnt3  27565  noresle  27650  nosupprefixmo  27653  noinfprefixmo  27654  addsprop  27913  mulsproplem9  28044  mulsasslem3  28085  readdscl  28247  tgjustf  28297  hlcgreu  28442  mirreu3  28478  cgraswap  28644  cgracom  28646  cgratr  28647  flatcgra  28648  acopyeu  28658  axsegcon  28758  ax5seglem9  28768  axeuclid  28794  axcontlem12  28806  clwwlkf1  29879  n4cyclfrgr  30121  frgrnbnb  30123  ablo4  30380  smcnlem  30527  pjhthmo  31132  pjpjpre  31249  3oalem2  31493  lnconi  31863  atom1d  32183  resf1o  32533  mgcoval  32734  xrge0tsmsd  32792  erlval  32997  ballotlemfc0  34145  ballotlemfcc  34146  pconnconn  34874  cvmfolem  34922  cvmliftmo  34927  cvmliftlem7  34934  cvmlift2lem10  34955  cvmlift3lem8  34969  lineext  35705  linecgr  35710  btwnconn1lem10  35725  btwnconn1lem11  35726  btwnconn3  35732  brsegle  35737  seglecgr12im  35739  segleantisym  35744  outsideoftr  35758  outsideofeq  35759  outsideofeu  35760  linethru  35782  finminlem  35835  neibastop2lem  35877  isbasisrelowllem1  36867  isbasisrelowllem2  36868  mblfinlem3  37165  ftc1cnnc  37198  isbnd3  37290  heibor1lem  37315  crngm4  37509  cvlcvr1  38843  4atlem12  39117  paddasslem12  39336  paddasslem13  39337  lhpexle2lem  39514  trlord  40074  cdlemkid4  40439  dihopelvalcpre  40753  dihmeetlem1N  40795  dihglblem5apreN  40796  dihmeetlem6  40814  dih1dimatlem0  40833  dihjatcclem4  40926  prjspner1  42081  mzpcl2  42181  mzpmfp  42198  mzpcompact2lem  42202  diophin  42223  pell14qrmulcl  42314  hbtlem2  42579  iunrelexpuztr  43180  stoweidlem61  45478  fourierdlem92  45615  euoreqb  46518  prproropf1olem3  46874  prproropf1olem4  46875  fpprwpprb  47109  snlindsntor  47617  elfzolborelfzop1  47665  nn0sumshdiglemB  47771