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 727	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  7323  fliftfun  7348  fprresex  8351  wfrlem17OLD  8381  domunfican  9389  finsschain  9429  suppeqfsuppbi  9448  fsuppunbi  9458  wemapsolem  9619  wemapso  9620  wemapso2lem  9621  cantnf  9762  enfin2i  10390  ttukeylem7  10584  fpwwe2lem2  10701  fpwwe2lem8  10707  fpwwe2lem11  10710  fpwwelem  10714  distrlem4pr  11095  mulcmpblnr  11140  prsrlem1  11141  addsrmo  11142  mulsrmo  11143  divdivdiv  11995  divsubdiv  12010  lediv12a  12188  xmullem  13326  xlemul1a  13350  seqcaopr  14090  leexp2r  14224  hashf1lem1  14504  hashf1lem2  14505  fi1uzind  14556  brfi1indALT  14559  wrd2ind  14771  swrdccat  14783  cshweqrep  14869  rtrclreclem4  15110  summolem2  15764  summo  15765  prodmolem2  15983  prodmo  15984  bezoutlem3  16588  bezoutlem4  16589  qredeu  16705  pcadd  16936  vdwlem9  17036  vdwlem10  17037  ramub1lem2  17074  ramub1  17075  cofucl  17952  setcmon  18154  poslubmo  18481  posglbmo  18482  grprcan  19013  isnsg3  19200  ghmpreima  19278  gaorber  19348  psgneu  19548  odcau  19646  lsmsubm  19695  lsmmod  19717  efgsfo  19781  ablfaclem3  20131  rngpropd  20201  ringpropd  20311  islmodd  20886  lmodprop2d  20944  lss1d  20984  lindff1  21863  islindf4  21881  assamulgscmlem2  21943  mplcoe1  22078  mplcoe5  22081  evlslem1  22129  mdetunilem7  22645  mdetunilem8  22646  mdetunilem9  22647  mdetuni0  22648  mdetmul  22650  ppttop  23035  epttop  23037  cnhaus  23383  isreg2  23406  cncmp  23421  1stcfb  23474  2ndcomap  23487  cldllycmp  23524  txcls  23633  ptclsg  23644  ptcnp  23651  txdis1cn  23664  txlly  23665  txnlly  23666  pthaus  23667  txhaus  23676  txkgen  23681  xkohaus  23682  xkococnlem  23688  xkococn  23689  fgabs  23908  rnelfm  23982  hausflimi  24009  hausflim  24010  alexsubALTlem2  24077  alexsubALTlem4  24079  alexsubALT  24080  tgpconncomp  24142  qustgplem  24150  metequiv2  24544  met2ndci  24556  nrmmetd  24608  nlmvscnlem1  24728  reconn  24869  xrge0tsms  24875  ipcnlem1  25298  minveclem3  25482  pmltpc  25504  ovolicc2lem5  25575  ovolicc2  25576  uniioombllem6  25642  dyadmbllem  25653  vitalilem3  25664  mbfmullem  25780  itg2split  25804  itg2mono  25808  bddiblnc  25897  dvlip2  26054  lhop1  26073  dvcnvrelem1  26076  ftc1lem6  26102  itgsubst  26110  dgrco  26335  plyexmo  26373  ulmdvlem3  26463  abelthlem2  26494  abelthlem8  26501  mpodvdsmulf1o  27255  dvdsmulf1o  27257  chpchtsum  27281  dchrptlem2  27327  2sqlem5  27484  2sqlem9  27489  2sqb  27494  pntrlog2bnd  27646  pntibndlem3  27654  pntlemp  27672  pnt3  27674  noresle  27760  nosupprefixmo  27763  noinfprefixmo  27764  addsprop  28027  mulsproplem9  28168  mulsasslem3  28209  readdscl  28449  tgjustf  28499  hlcgreu  28644  mirreu3  28680  cgraswap  28846  cgracom  28848  cgratr  28849  flatcgra  28850  acopyeu  28860  axsegcon  28960  ax5seglem9  28970  axeuclid  28996  axcontlem12  29008  clwwlkf1  30081  n4cyclfrgr  30323  frgrnbnb  30325  ablo4  30582  smcnlem  30729  pjhthmo  31334  pjpjpre  31451  3oalem2  31695  lnconi  32065  atom1d  32385  resf1o  32744  mgcoval  32959  xrge0tsmsd  33041  erlval  33230  ballotlemfc0  34457  ballotlemfcc  34458  pconnconn  35199  cvmfolem  35247  cvmliftmo  35252  cvmliftlem7  35259  cvmlift2lem10  35280  cvmlift3lem8  35294  lineext  36040  linecgr  36045  btwnconn1lem10  36060  btwnconn1lem11  36061  btwnconn3  36067  brsegle  36072  seglecgr12im  36074  segleantisym  36079  outsideoftr  36093  outsideofeq  36094  outsideofeu  36095  linethru  36117  finminlem  36284  neibastop2lem  36326  weiunpo  36431  isbasisrelowllem1  37321  isbasisrelowllem2  37322  mblfinlem3  37619  ftc1cnnc  37652  isbnd3  37744  heibor1lem  37769  crngm4  37963  cvlcvr1  39295  4atlem12  39569  paddasslem12  39788  paddasslem13  39789  lhpexle2lem  39966  trlord  40526  cdlemkid4  40891  dihopelvalcpre  41205  dihmeetlem1N  41247  dihglblem5apreN  41248  dihmeetlem6  41266  dih1dimatlem0  41285  dihjatcclem4  41378  unitscyglem4  42155  prjspner1  42581  mzpcl2  42686  mzpmfp  42703  mzpcompact2lem  42707  diophin  42728  pell14qrmulcl  42819  hbtlem2  43081  iunrelexpuztr  43681  stoweidlem61  45982  fourierdlem92  46119  euoreqb  47024  prproropf1olem3  47379  prproropf1olem4  47380  fpprwpprb  47614  grimgrtri  47798  snlindsntor  48200  elfzolborelfzop1  48248  nn0sumshdiglemB  48354