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

This theorem is referenced by:  fcof1  7290  fliftfun  7314  fprresex  8309  wfrlem17OLD  8339  domunfican  9338  finsschain  9377  suppeqfsuppbi  9396  fsuppunbi  9406  wemapsolem  9567  wemapso  9568  wemapso2lem  9569  cantnf  9710  enfin2i  10338  ttukeylem7  10532  fpwwe2lem2  10649  fpwwe2lem8  10655  fpwwe2lem11  10658  fpwwelem  10662  distrlem4pr  11043  mulcmpblnr  11088  prsrlem1  11089  addsrmo  11090  mulsrmo  11091  divdivdiv  11939  divsubdiv  11954  lediv12a  12131  xmullem  13269  xlemul1a  13293  seqcaopr  14030  leexp2r  14164  hashf1lem1  14441  hashf1lem1OLD  14442  hashf1lem2  14443  fi1uzind  14484  brfi1indALT  14487  wrd2ind  14699  swrdccat  14711  cshweqrep  14797  rtrclreclem4  15034  summolem2  15688  summo  15689  prodmolem2  15905  prodmo  15906  bezoutlem3  16510  bezoutlem4  16511  qredeu  16622  pcadd  16851  vdwlem9  16951  vdwlem10  16952  ramub1lem2  16989  ramub1  16990  cofucl  17867  setcmon  18069  poslubmo  18396  posglbmo  18397  grprcan  18923  isnsg3  19108  ghmpreima  19185  gaorber  19252  psgneu  19454  odcau  19552  lsmsubm  19601  lsmmod  19623  efgsfo  19687  ablfaclem3  20037  rngpropd  20107  ringpropd  20217  islmodd  20742  lmodprop2d  20800  lss1d  20840  lindff1  21747  islindf4  21765  assamulgscmlem2  21826  mplcoe1  21968  mplcoe5  21971  evlslem1  22021  mdetunilem7  22513  mdetunilem8  22514  mdetunilem9  22515  mdetuni0  22516  mdetmul  22518  ppttop  22903  epttop  22905  cnhaus  23251  isreg2  23274  cncmp  23289  1stcfb  23342  2ndcomap  23355  cldllycmp  23392  txcls  23501  ptclsg  23512  ptcnp  23519  txdis1cn  23532  txlly  23533  txnlly  23534  pthaus  23535  txhaus  23544  txkgen  23549  xkohaus  23550  xkococnlem  23556  xkococn  23557  fgabs  23776  rnelfm  23850  hausflimi  23877  hausflim  23878  alexsubALTlem2  23945  alexsubALTlem4  23947  alexsubALT  23948  tgpconncomp  24010  qustgplem  24018  metequiv2  24412  met2ndci  24424  nrmmetd  24476  nlmvscnlem1  24596  reconn  24737  xrge0tsms  24743  ipcnlem1  25166  minveclem3  25350  pmltpc  25372  ovolicc2lem5  25443  ovolicc2  25444  uniioombllem6  25510  dyadmbllem  25521  vitalilem3  25532  mbfmullem  25648  itg2split  25672  itg2mono  25676  bddiblnc  25764  dvlip2  25921  lhop1  25940  dvcnvrelem1  25943  ftc1lem6  25969  itgsubst  25977  dgrco  26203  plyexmo  26241  ulmdvlem3  26331  abelthlem2  26362  abelthlem8  26369  mpodvdsmulf1o  27119  dvdsmulf1o  27121  chpchtsum  27145  dchrptlem2  27191  2sqlem5  27348  2sqlem9  27353  2sqb  27358  pntrlog2bnd  27510  pntibndlem3  27518  pntlemp  27536  pnt3  27538  noresle  27623  nosupprefixmo  27626  noinfprefixmo  27627  addsprop  27886  mulsproplem9  28017  mulsasslem3  28058  readdscl  28220  tgjustf  28270  hlcgreu  28415  mirreu3  28451  cgraswap  28617  cgracom  28619  cgratr  28620  flatcgra  28621  acopyeu  28631  axsegcon  28731  ax5seglem9  28741  axeuclid  28767  axcontlem12  28779  clwwlkf1  29852  n4cyclfrgr  30094  frgrnbnb  30096  ablo4  30353  smcnlem  30500  pjhthmo  31105  pjpjpre  31222  3oalem2  31466  lnconi  31836  atom1d  32156  resf1o  32506  mgcoval  32707  xrge0tsmsd  32765  erlval  32966  ballotlemfc0  34106  ballotlemfcc  34107  pconnconn  34835  cvmfolem  34883  cvmliftmo  34888  cvmliftlem7  34895  cvmlift2lem10  34916  cvmlift3lem8  34930  lineext  35666  linecgr  35671  btwnconn1lem10  35686  btwnconn1lem11  35687  btwnconn3  35693  brsegle  35698  seglecgr12im  35700  segleantisym  35705  outsideoftr  35719  outsideofeq  35720  outsideofeu  35721  linethru  35743  finminlem  35796  neibastop2lem  35838  isbasisrelowllem1  36828  isbasisrelowllem2  36829  mblfinlem3  37126  ftc1cnnc  37159  isbnd3  37251  heibor1lem  37276  crngm4  37470  cvlcvr1  38805  4atlem12  39079  paddasslem12  39298  paddasslem13  39299  lhpexle2lem  39476  trlord  40036  cdlemkid4  40401  dihopelvalcpre  40715  dihmeetlem1N  40757  dihglblem5apreN  40758  dihmeetlem6  40776  dih1dimatlem0  40795  dihjatcclem4  40888  prjspner1  42044  mzpcl2  42144  mzpmfp  42161  mzpcompact2lem  42165  diophin  42186  pell14qrmulcl  42277  hbtlem2  42542  iunrelexpuztr  43143  stoweidlem61  45443  fourierdlem92  45580  euoreqb  46483  prproropf1olem3  46839  prproropf1olem4  46840  fpprwpprb  47074  snlindsntor  47533  elfzolborelfzop1  47581  nn0sumshdiglemB  47687