Theorem simprlr 776

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 724	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 206  df-an 396

This theorem is referenced by:  fcof1  7139  fliftfun  7163  fprresex  8097  wfrlem17OLD  8127  domunfican  9017  finsschain  9056  suppeqfsuppbi  9072  fsuppunbi  9079  wemapsolem  9239  wemapso  9240  wemapso2lem  9241  cantnf  9381  enfin2i  10008  ttukeylem7  10202  fpwwe2lem2  10319  fpwwe2lem8  10325  fpwwe2lem11  10328  fpwwelem  10332  distrlem4pr  10713  mulcmpblnr  10758  prsrlem1  10759  addsrmo  10760  mulsrmo  10761  divdivdiv  11606  divsubdiv  11621  lediv12a  11798  xmullem  12927  xlemul1a  12951  seqcaopr  13688  leexp2r  13820  hashf1lem1  14096  hashf1lem1OLD  14097  hashf1lem2  14098  fi1uzind  14139  brfi1indALT  14142  wrd2ind  14364  swrdccat  14376  cshweqrep  14462  rtrclreclem4  14700  summolem2  15356  summo  15357  prodmolem2  15573  prodmo  15574  bezoutlem3  16177  bezoutlem4  16178  qredeu  16291  pcadd  16518  vdwlem9  16618  vdwlem10  16619  ramub1lem2  16656  ramub1  16657  cofucl  17519  setcmon  17718  poslubmo  18044  posglbmo  18045  grprcan  18528  isnsg3  18703  ghmpreima  18771  gaorber  18829  psgneu  19029  odcau  19124  lsmsubm  19173  lsmmod  19196  efgsfo  19260  ablfaclem3  19605  ringpropd  19736  islmodd  20044  lmodprop2d  20100  lss1d  20140  lindff1  20937  islindf4  20955  assamulgscmlem2  21014  mplcoe1  21148  mplcoe5  21151  evlslem1  21202  mdetunilem7  21675  mdetunilem8  21676  mdetunilem9  21677  mdetuni0  21678  mdetmul  21680  ppttop  22065  epttop  22067  cnhaus  22413  isreg2  22436  cncmp  22451  1stcfb  22504  2ndcomap  22517  cldllycmp  22554  txcls  22663  ptclsg  22674  ptcnp  22681  txdis1cn  22694  txlly  22695  txnlly  22696  pthaus  22697  txhaus  22706  txkgen  22711  xkohaus  22712  xkococnlem  22718  xkococn  22719  fgabs  22938  rnelfm  23012  hausflimi  23039  hausflim  23040  alexsubALTlem2  23107  alexsubALTlem4  23109  alexsubALT  23110  tgpconncomp  23172  qustgplem  23180  metequiv2  23572  met2ndci  23584  nrmmetd  23636  nlmvscnlem1  23756  reconn  23897  xrge0tsms  23903  ipcnlem1  24314  minveclem3  24498  pmltpc  24519  ovolicc2lem5  24590  ovolicc2  24591  uniioombllem6  24657  dyadmbllem  24668  vitalilem3  24679  mbfmullem  24795  itg2split  24819  itg2mono  24823  bddiblnc  24911  dvlip2  25064  lhop1  25083  dvcnvrelem1  25086  ftc1lem6  25110  itgsubst  25118  dgrco  25341  plyexmo  25378  ulmdvlem3  25466  abelthlem2  25496  abelthlem8  25503  dvdsmulf1o  26248  chpchtsum  26272  dchrptlem2  26318  2sqlem5  26475  2sqlem9  26480  2sqb  26485  pntrlog2bnd  26637  pntibndlem3  26645  pntlemp  26663  pnt3  26665  tgjustf  26738  hlcgreu  26883  mirreu3  26919  cgraswap  27085  cgracom  27087  cgratr  27088  flatcgra  27089  acopyeu  27099  axsegcon  27198  ax5seglem9  27208  axeuclid  27234  axcontlem12  27246  clwwlkf1  28314  n4cyclfrgr  28556  frgrnbnb  28558  ablo4  28813  smcnlem  28960  pjhthmo  29565  pjpjpre  29682  3oalem2  29926  lnconi  30296  atom1d  30616  resf1o  30967  mgcoval  31166  xrge0tsmsd  31219  ballotlemfc0  32359  ballotlemfcc  32360  pconnconn  33093  cvmfolem  33141  cvmliftmo  33146  cvmliftlem7  33153  cvmlift2lem10  33174  cvmlift3lem8  33188  noresle  33827  nosupprefixmo  33830  noinfprefixmo  33831  lineext  34305  linecgr  34310  btwnconn1lem10  34325  btwnconn1lem11  34326  btwnconn3  34332  brsegle  34337  seglecgr12im  34339  segleantisym  34344  outsideoftr  34358  outsideofeq  34359  outsideofeu  34360  linethru  34382  finminlem  34434  neibastop2lem  34476  isbasisrelowllem1  35453  isbasisrelowllem2  35454  mblfinlem3  35743  ftc1cnnc  35776  isbnd3  35869  heibor1lem  35894  crngm4  36088  cvlcvr1  37280  4atlem12  37553  paddasslem12  37772  paddasslem13  37773  lhpexle2lem  37950  trlord  38510  cdlemkid4  38875  dihopelvalcpre  39189  dihmeetlem1N  39231  dihglblem5apreN  39232  dihmeetlem6  39250  dih1dimatlem0  39269  dihjatcclem4  39362  prjspner1  40384  mzpcl2  40468  mzpmfp  40485  mzpcompact2lem  40489  diophin  40510  pell14qrmulcl  40601  hbtlem2  40865  iunrelexpuztr  41216  stoweidlem61  43492  fourierdlem92  43629  euoreqb  44488  prproropf1olem3  44845  prproropf1olem4  44846  fpprwpprb  45080  snlindsntor  45700  elfzolborelfzop1  45748  nn0sumshdiglemB  45854