Theorem simprlr 778

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  fcof1  7284  fliftfun  7308  fprresex  8294  wfrlem17OLD  8324  domunfican  9319  finsschain  9358  suppeqfsuppbi  9376  fsuppunbi  9383  wemapsolem  9544  wemapso  9545  wemapso2lem  9546  cantnf  9687  enfin2i  10315  ttukeylem7  10509  fpwwe2lem2  10626  fpwwe2lem8  10632  fpwwe2lem11  10635  fpwwelem  10639  distrlem4pr  11020  mulcmpblnr  11065  prsrlem1  11066  addsrmo  11067  mulsrmo  11068  divdivdiv  11914  divsubdiv  11929  lediv12a  12106  xmullem  13242  xlemul1a  13266  seqcaopr  14004  leexp2r  14138  hashf1lem1  14414  hashf1lem1OLD  14415  hashf1lem2  14416  fi1uzind  14457  brfi1indALT  14460  wrd2ind  14672  swrdccat  14684  cshweqrep  14770  rtrclreclem4  15007  summolem2  15661  summo  15662  prodmolem2  15878  prodmo  15879  bezoutlem3  16482  bezoutlem4  16483  qredeu  16594  pcadd  16821  vdwlem9  16921  vdwlem10  16922  ramub1lem2  16959  ramub1  16960  cofucl  17837  setcmon  18036  poslubmo  18363  posglbmo  18364  grprcan  18857  isnsg3  19039  ghmpreima  19113  gaorber  19171  psgneu  19373  odcau  19471  lsmsubm  19520  lsmmod  19542  efgsfo  19606  ablfaclem3  19956  ringpropd  20101  islmodd  20476  lmodprop2d  20533  lss1d  20573  lindff1  21374  islindf4  21392  assamulgscmlem2  21453  mplcoe1  21591  mplcoe5  21594  evlslem1  21644  mdetunilem7  22119  mdetunilem8  22120  mdetunilem9  22121  mdetuni0  22122  mdetmul  22124  ppttop  22509  epttop  22511  cnhaus  22857  isreg2  22880  cncmp  22895  1stcfb  22948  2ndcomap  22961  cldllycmp  22998  txcls  23107  ptclsg  23118  ptcnp  23125  txdis1cn  23138  txlly  23139  txnlly  23140  pthaus  23141  txhaus  23150  txkgen  23155  xkohaus  23156  xkococnlem  23162  xkococn  23163  fgabs  23382  rnelfm  23456  hausflimi  23483  hausflim  23484  alexsubALTlem2  23551  alexsubALTlem4  23553  alexsubALT  23554  tgpconncomp  23616  qustgplem  23624  metequiv2  24018  met2ndci  24030  nrmmetd  24082  nlmvscnlem1  24202  reconn  24343  xrge0tsms  24349  ipcnlem1  24761  minveclem3  24945  pmltpc  24966  ovolicc2lem5  25037  ovolicc2  25038  uniioombllem6  25104  dyadmbllem  25115  vitalilem3  25126  mbfmullem  25242  itg2split  25266  itg2mono  25270  bddiblnc  25358  dvlip2  25511  lhop1  25530  dvcnvrelem1  25533  ftc1lem6  25557  itgsubst  25565  dgrco  25788  plyexmo  25825  ulmdvlem3  25913  abelthlem2  25943  abelthlem8  25950  dvdsmulf1o  26695  chpchtsum  26719  dchrptlem2  26765  2sqlem5  26922  2sqlem9  26927  2sqb  26932  pntrlog2bnd  27084  pntibndlem3  27092  pntlemp  27110  pnt3  27112  noresle  27197  nosupprefixmo  27200  noinfprefixmo  27201  addsprop  27457  mulsproplem9  27577  mulsasslem3  27617  tgjustf  27721  hlcgreu  27866  mirreu3  27902  cgraswap  28068  cgracom  28070  cgratr  28071  flatcgra  28072  acopyeu  28082  axsegcon  28182  ax5seglem9  28192  axeuclid  28218  axcontlem12  28230  clwwlkf1  29299  n4cyclfrgr  29541  frgrnbnb  29543  ablo4  29798  smcnlem  29945  pjhthmo  30550  pjpjpre  30667  3oalem2  30911  lnconi  31281  atom1d  31601  resf1o  31950  mgcoval  32151  xrge0tsmsd  32204  ballotlemfc0  33486  ballotlemfcc  33487  pconnconn  34217  cvmfolem  34265  cvmliftmo  34270  cvmliftlem7  34277  cvmlift2lem10  34298  cvmlift3lem8  34312  lineext  35043  linecgr  35048  btwnconn1lem10  35063  btwnconn1lem11  35064  btwnconn3  35070  brsegle  35075  seglecgr12im  35077  segleantisym  35082  outsideoftr  35096  outsideofeq  35097  outsideofeu  35098  linethru  35120  finminlem  35198  neibastop2lem  35240  isbasisrelowllem1  36231  isbasisrelowllem2  36232  mblfinlem3  36522  ftc1cnnc  36555  isbnd3  36647  heibor1lem  36672  crngm4  36866  cvlcvr1  38204  4atlem12  38478  paddasslem12  38697  paddasslem13  38698  lhpexle2lem  38875  trlord  39435  cdlemkid4  39800  dihopelvalcpre  40114  dihmeetlem1N  40156  dihglblem5apreN  40157  dihmeetlem6  40175  dih1dimatlem0  40194  dihjatcclem4  40287  prjspner1  41369  mzpcl2  41458  mzpmfp  41475  mzpcompact2lem  41479  diophin  41500  pell14qrmulcl  41591  hbtlem2  41856  iunrelexpuztr  42460  stoweidlem61  44767  fourierdlem92  44904  euoreqb  45807  prproropf1olem3  46163  prproropf1olem4  46164  fpprwpprb  46398  rngpropd  46663  snlindsntor  47142  elfzolborelfzop1  47190  nn0sumshdiglemB  47296