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  7279  fliftfun  7304  fprresex  8307  wfrlem17OLD  8337  domunfican  9331  finsschain  9369  suppeqfsuppbi  9389  fsuppunbi  9399  wemapsolem  9562  wemapso  9563  wemapso2lem  9564  cantnf  9705  enfin2i  10333  ttukeylem7  10527  fpwwe2lem2  10644  fpwwe2lem8  10650  fpwwe2lem11  10653  fpwwelem  10657  distrlem4pr  11038  mulcmpblnr  11083  prsrlem1  11084  addsrmo  11085  mulsrmo  11086  divdivdiv  11940  divsubdiv  11955  lediv12a  12133  xmullem  13278  xlemul1a  13302  seqcaopr  14055  leexp2r  14190  hashf1lem1  14471  hashf1lem2  14472  fi1uzind  14523  brfi1indALT  14526  wrd2ind  14739  swrdccat  14751  cshweqrep  14837  rtrclreclem4  15078  summolem2  15730  summo  15731  prodmolem2  15949  prodmo  15950  bezoutlem3  16558  bezoutlem4  16559  qredeu  16675  pcadd  16907  vdwlem9  17007  vdwlem10  17008  ramub1lem2  17045  ramub1  17046  cofucl  17899  setcmon  18098  poslubmo  18419  posglbmo  18420  grprcan  18954  isnsg3  19141  ghmpreima  19219  gaorber  19289  psgneu  19485  odcau  19583  lsmsubm  19632  lsmmod  19654  efgsfo  19718  ablfaclem3  20068  rngpropd  20132  ringpropd  20246  islmodd  20821  lmodprop2d  20879  lss1d  20918  lindff1  21778  islindf4  21796  assamulgscmlem2  21858  mplcoe1  21993  mplcoe5  21996  evlslem1  22038  mdetunilem7  22554  mdetunilem8  22555  mdetunilem9  22556  mdetuni0  22557  mdetmul  22559  ppttop  22943  epttop  22945  cnhaus  23290  isreg2  23313  cncmp  23328  1stcfb  23381  2ndcomap  23394  cldllycmp  23431  txcls  23540  ptclsg  23551  ptcnp  23558  txdis1cn  23571  txlly  23572  txnlly  23573  pthaus  23574  txhaus  23583  txkgen  23588  xkohaus  23589  xkococnlem  23595  xkococn  23596  fgabs  23815  rnelfm  23889  hausflimi  23916  hausflim  23917  alexsubALTlem2  23984  alexsubALTlem4  23986  alexsubALT  23987  tgpconncomp  24049  qustgplem  24057  metequiv2  24447  met2ndci  24459  nrmmetd  24511  nlmvscnlem1  24623  reconn  24766  xrge0tsms  24772  ipcnlem1  25195  minveclem3  25379  pmltpc  25401  ovolicc2lem5  25472  ovolicc2  25473  uniioombllem6  25539  dyadmbllem  25550  vitalilem3  25561  mbfmullem  25676  itg2split  25700  itg2mono  25704  bddiblnc  25793  dvlip2  25950  lhop1  25969  dvcnvrelem1  25972  ftc1lem6  25998  itgsubst  26006  dgrco  26231  plyexmo  26271  ulmdvlem3  26361  abelthlem2  26392  abelthlem8  26399  mpodvdsmulf1o  27154  dvdsmulf1o  27156  chpchtsum  27180  dchrptlem2  27226  2sqlem5  27383  2sqlem9  27388  2sqb  27393  pntrlog2bnd  27545  pntibndlem3  27553  pntlemp  27571  pnt3  27573  noresle  27659  nosupprefixmo  27662  noinfprefixmo  27663  addsprop  27926  mulsproplem9  28067  mulsasslem3  28108  readdscl  28348  tgjustf  28398  hlcgreu  28543  mirreu3  28579  cgraswap  28745  cgracom  28747  cgratr  28748  flatcgra  28749  acopyeu  28759  axsegcon  28852  ax5seglem9  28862  axeuclid  28888  axcontlem12  28900  clwwlkf1  29976  n4cyclfrgr  30218  frgrnbnb  30220  ablo4  30477  smcnlem  30624  pjhthmo  31229  pjpjpre  31346  3oalem2  31590  lnconi  31960  atom1d  32280  resf1o  32653  mgcoval  32912  xrge0tsmsd  33002  erlval  33199  ballotlemfc0  34471  ballotlemfcc  34472  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  36282  neibastop2lem  36324  weiunpo  36429  isbasisrelowllem1  37319  isbasisrelowllem2  37320  mblfinlem3  37629  ftc1cnnc  37662  isbnd3  37754  heibor1lem  37779  crngm4  37973  cvlcvr1  39303  4atlem12  39577  paddasslem12  39796  paddasslem13  39797  lhpexle2lem  39974  trlord  40534  cdlemkid4  40899  dihopelvalcpre  41213  dihmeetlem1N  41255  dihglblem5apreN  41256  dihmeetlem6  41274  dih1dimatlem0  41293  dihjatcclem4  41386  unitscyglem4  42157  prjspner1  42596  mzpcl2  42700  mzpmfp  42717  mzpcompact2lem  42721  diophin  42742  pell14qrmulcl  42833  hbtlem2  43095  iunrelexpuztr  43690  stoweidlem61  46038  fourierdlem92  46175  euoreqb  47086  prproropf1olem3  47467  prproropf1olem4  47468  fpprwpprb  47702  cycldlenngric  47889  grimgrtri  47909  snlindsntor  48395  elfzolborelfzop1  48443  nn0sumshdiglemB  48548  2arwcat  49425