Theorem simprlr 779

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  7264  fliftfun  7289  fprresex  8291  domunfican  9278  finsschain  9316  suppeqfsuppbi  9336  fsuppunbi  9346  wemapsolem  9509  wemapso  9510  wemapso2lem  9511  cantnf  9652  enfin2i  10280  ttukeylem7  10474  fpwwe2lem2  10591  fpwwe2lem8  10597  fpwwe2lem11  10600  fpwwelem  10604  distrlem4pr  10985  mulcmpblnr  11030  prsrlem1  11031  addsrmo  11032  mulsrmo  11033  divdivdiv  11889  divsubdiv  11904  lediv12a  12082  xmullem  13230  xlemul1a  13254  seqcaopr  14010  leexp2r  14145  hashf1lem1  14426  hashf1lem2  14427  fi1uzind  14478  brfi1indALT  14481  wrd2ind  14694  swrdccat  14706  cshweqrep  14792  rtrclreclem4  15033  summolem2  15688  summo  15689  prodmolem2  15907  prodmo  15908  bezoutlem3  16517  bezoutlem4  16518  qredeu  16634  pcadd  16866  vdwlem9  16966  vdwlem10  16967  ramub1lem2  17004  ramub1  17005  cofucl  17856  setcmon  18055  poslubmo  18376  posglbmo  18377  grprcan  18911  isnsg3  19098  ghmpreima  19176  gaorber  19246  psgneu  19442  odcau  19540  lsmsubm  19589  lsmmod  19611  efgsfo  19675  ablfaclem3  20025  rngpropd  20089  ringpropd  20203  islmodd  20778  lmodprop2d  20836  lss1d  20875  lindff1  21735  islindf4  21753  assamulgscmlem2  21815  mplcoe1  21950  mplcoe5  21953  evlslem1  21995  mdetunilem7  22511  mdetunilem8  22512  mdetunilem9  22513  mdetuni0  22514  mdetmul  22516  ppttop  22900  epttop  22902  cnhaus  23247  isreg2  23270  cncmp  23285  1stcfb  23338  2ndcomap  23351  cldllycmp  23388  txcls  23497  ptclsg  23508  ptcnp  23515  txdis1cn  23528  txlly  23529  txnlly  23530  pthaus  23531  txhaus  23540  txkgen  23545  xkohaus  23546  xkococnlem  23552  xkococn  23553  fgabs  23772  rnelfm  23846  hausflimi  23873  hausflim  23874  alexsubALTlem2  23941  alexsubALTlem4  23943  alexsubALT  23944  tgpconncomp  24006  qustgplem  24014  metequiv2  24404  met2ndci  24416  nrmmetd  24468  nlmvscnlem1  24580  reconn  24723  xrge0tsms  24729  ipcnlem1  25151  minveclem3  25335  pmltpc  25357  ovolicc2lem5  25428  ovolicc2  25429  uniioombllem6  25495  dyadmbllem  25506  vitalilem3  25517  mbfmullem  25632  itg2split  25656  itg2mono  25660  bddiblnc  25749  dvlip2  25906  lhop1  25925  dvcnvrelem1  25928  ftc1lem6  25954  itgsubst  25962  dgrco  26187  plyexmo  26227  ulmdvlem3  26317  abelthlem2  26348  abelthlem8  26355  mpodvdsmulf1o  27110  dvdsmulf1o  27112  chpchtsum  27136  dchrptlem2  27182  2sqlem5  27339  2sqlem9  27344  2sqb  27349  pntrlog2bnd  27501  pntibndlem3  27509  pntlemp  27527  pnt3  27529  noresle  27615  nosupprefixmo  27618  noinfprefixmo  27619  addsprop  27889  mulsproplem9  28033  mulsasslem3  28074  onscutlt  28171  expadds  28326  readdscl  28356  tgjustf  28406  hlcgreu  28551  mirreu3  28587  cgraswap  28753  cgracom  28755  cgratr  28756  flatcgra  28757  acopyeu  28767  axsegcon  28860  ax5seglem9  28870  axeuclid  28896  axcontlem12  28908  clwwlkf1  29984  n4cyclfrgr  30226  frgrnbnb  30228  ablo4  30485  smcnlem  30632  pjhthmo  31237  pjpjpre  31354  3oalem2  31598  lnconi  31968  atom1d  32288  resf1o  32659  mgcoval  32918  xrge0tsmsd  33008  erlval  33215  ballotlemfc0  34490  ballotlemfcc  34491  pconnconn  35218  cvmfolem  35266  cvmliftmo  35271  cvmliftlem7  35278  cvmlift2lem10  35299  cvmlift3lem8  35313  lineext  36059  linecgr  36064  btwnconn1lem10  36079  btwnconn1lem11  36080  btwnconn3  36086  brsegle  36091  seglecgr12im  36093  segleantisym  36098  outsideoftr  36112  outsideofeq  36113  outsideofeu  36114  linethru  36136  finminlem  36301  neibastop2lem  36343  weiunpo  36448  isbasisrelowllem1  37338  isbasisrelowllem2  37339  mblfinlem3  37648  ftc1cnnc  37681  isbnd3  37773  heibor1lem  37798  crngm4  37992  cvlcvr1  39327  4atlem12  39601  paddasslem12  39820  paddasslem13  39821  lhpexle2lem  39998  trlord  40558  cdlemkid4  40923  dihopelvalcpre  41237  dihmeetlem1N  41279  dihglblem5apreN  41280  dihmeetlem6  41298  dih1dimatlem0  41317  dihjatcclem4  41410  unitscyglem4  42181  prjspner1  42607  mzpcl2  42711  mzpmfp  42728  mzpcompact2lem  42732  diophin  42753  pell14qrmulcl  42844  hbtlem2  43106  iunrelexpuztr  43701  stoweidlem61  46052  fourierdlem92  46189  euoreqb  47100  prproropf1olem3  47496  prproropf1olem4  47497  fpprwpprb  47731  cycldlenngric  47918  grimgrtri  47938  snlindsntor  48450  elfzolborelfzop1  48498  nn0sumshdiglemB  48599  2arwcat  49579