Theorem simprlr 780

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 484	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrl 728	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  fcof1  7307  fliftfun  7332  fprresex  8335  wfrlem17OLD  8365  domunfican  9361  finsschain  9399  suppeqfsuppbi  9419  fsuppunbi  9429  wemapsolem  9590  wemapso  9591  wemapso2lem  9592  cantnf  9733  enfin2i  10361  ttukeylem7  10555  fpwwe2lem2  10672  fpwwe2lem8  10678  fpwwe2lem11  10681  fpwwelem  10685  distrlem4pr  11066  mulcmpblnr  11111  prsrlem1  11112  addsrmo  11113  mulsrmo  11114  divdivdiv  11968  divsubdiv  11983  lediv12a  12161  xmullem  13306  xlemul1a  13330  seqcaopr  14080  leexp2r  14214  hashf1lem1  14494  hashf1lem2  14495  fi1uzind  14546  brfi1indALT  14549  wrd2ind  14761  swrdccat  14773  cshweqrep  14859  rtrclreclem4  15100  summolem2  15752  summo  15753  prodmolem2  15971  prodmo  15972  bezoutlem3  16578  bezoutlem4  16579  qredeu  16695  pcadd  16927  vdwlem9  17027  vdwlem10  17028  ramub1lem2  17065  ramub1  17066  cofucl  17933  setcmon  18132  poslubmo  18456  posglbmo  18457  grprcan  18991  isnsg3  19178  ghmpreima  19256  gaorber  19326  psgneu  19524  odcau  19622  lsmsubm  19671  lsmmod  19693  efgsfo  19757  ablfaclem3  20107  rngpropd  20171  ringpropd  20285  islmodd  20864  lmodprop2d  20922  lss1d  20961  lindff1  21840  islindf4  21858  assamulgscmlem2  21920  mplcoe1  22055  mplcoe5  22058  evlslem1  22106  mdetunilem7  22624  mdetunilem8  22625  mdetunilem9  22626  mdetuni0  22627  mdetmul  22629  ppttop  23014  epttop  23016  cnhaus  23362  isreg2  23385  cncmp  23400  1stcfb  23453  2ndcomap  23466  cldllycmp  23503  txcls  23612  ptclsg  23623  ptcnp  23630  txdis1cn  23643  txlly  23644  txnlly  23645  pthaus  23646  txhaus  23655  txkgen  23660  xkohaus  23661  xkococnlem  23667  xkococn  23668  fgabs  23887  rnelfm  23961  hausflimi  23988  hausflim  23989  alexsubALTlem2  24056  alexsubALTlem4  24058  alexsubALT  24059  tgpconncomp  24121  qustgplem  24129  metequiv2  24523  met2ndci  24535  nrmmetd  24587  nlmvscnlem1  24707  reconn  24850  xrge0tsms  24856  ipcnlem1  25279  minveclem3  25463  pmltpc  25485  ovolicc2lem5  25556  ovolicc2  25557  uniioombllem6  25623  dyadmbllem  25634  vitalilem3  25645  mbfmullem  25760  itg2split  25784  itg2mono  25788  bddiblnc  25877  dvlip2  26034  lhop1  26053  dvcnvrelem1  26056  ftc1lem6  26082  itgsubst  26090  dgrco  26315  plyexmo  26355  ulmdvlem3  26445  abelthlem2  26476  abelthlem8  26483  mpodvdsmulf1o  27237  dvdsmulf1o  27239  chpchtsum  27263  dchrptlem2  27309  2sqlem5  27466  2sqlem9  27471  2sqb  27476  pntrlog2bnd  27628  pntibndlem3  27636  pntlemp  27654  pnt3  27656  noresle  27742  nosupprefixmo  27745  noinfprefixmo  27746  addsprop  28009  mulsproplem9  28150  mulsasslem3  28191  readdscl  28431  tgjustf  28481  hlcgreu  28626  mirreu3  28662  cgraswap  28828  cgracom  28830  cgratr  28831  flatcgra  28832  acopyeu  28842  axsegcon  28942  ax5seglem9  28952  axeuclid  28978  axcontlem12  28990  clwwlkf1  30068  n4cyclfrgr  30310  frgrnbnb  30312  ablo4  30569  smcnlem  30716  pjhthmo  31321  pjpjpre  31438  3oalem2  31682  lnconi  32052  atom1d  32372  resf1o  32741  mgcoval  32976  xrge0tsmsd  33065  erlval  33262  ballotlemfc0  34495  ballotlemfcc  34496  pconnconn  35236  cvmfolem  35284  cvmliftmo  35289  cvmliftlem7  35296  cvmlift2lem10  35317  cvmlift3lem8  35331  lineext  36077  linecgr  36082  btwnconn1lem10  36097  btwnconn1lem11  36098  btwnconn3  36104  brsegle  36109  seglecgr12im  36111  segleantisym  36116  outsideoftr  36130  outsideofeq  36131  outsideofeu  36132  linethru  36154  finminlem  36319  neibastop2lem  36361  weiunpo  36466  isbasisrelowllem1  37356  isbasisrelowllem2  37357  mblfinlem3  37666  ftc1cnnc  37699  isbnd3  37791  heibor1lem  37816  crngm4  38010  cvlcvr1  39340  4atlem12  39614  paddasslem12  39833  paddasslem13  39834  lhpexle2lem  40011  trlord  40571  cdlemkid4  40936  dihopelvalcpre  41250  dihmeetlem1N  41292  dihglblem5apreN  41293  dihmeetlem6  41311  dih1dimatlem0  41330  dihjatcclem4  41423  unitscyglem4  42199  prjspner1  42636  mzpcl2  42741  mzpmfp  42758  mzpcompact2lem  42762  diophin  42783  pell14qrmulcl  42874  hbtlem2  43136  iunrelexpuztr  43732  stoweidlem61  46076  fourierdlem92  46213  euoreqb  47121  prproropf1olem3  47492  prproropf1olem4  47493  fpprwpprb  47727  grimgrtri  47916  snlindsntor  48388  elfzolborelfzop1  48436  nn0sumshdiglemB  48541