Theorem simprlr 803

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  disjxiunOLD  4650  fcof1  6542  fliftfun  6562  wfrlem17  7431  domunfican  8233  finsschain  8273  suppeqfsuppbi  8289  fsuppunbi  8296  wemapsolem  8455  wemapso  8456  wemapso2lem  8457  cantnf  8590  enfin2i  9143  ttukeylem7  9337  fpwwe2lem2  9454  fpwwe2lem9  9460  fpwwe2lem12  9463  fpwwelem  9467  distrlem4pr  9848  mulcmpblnr  9892  prsrlem1  9893  addsrmo  9894  mulsrmo  9895  divdivdiv  10726  divsubdiv  10741  lediv12a  10916  xmullem  12094  xlemul1a  12118  seqcaopr  12838  leexp2r  12918  hashf1lem1  13239  hashf1lem2  13240  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  wrd2ind  13477  cshweqrep  13567  summolem2  14447  summo  14448  prodmolem2  14665  prodmo  14666  bezoutlem3  15258  bezoutlem4  15259  qredeu  15372  pcadd  15593  vdwlem9  15693  vdwlem10  15694  ramub1lem2  15731  ramub1  15732  cofucl  16548  setcmon  16737  poslubmo  17146  posglbmo  17147  grprcan  17455  isnsg3  17628  ghmpreima  17682  gaorber  17741  psgneu  17926  odcau  18019  lsmsubm  18068  lsmmod  18088  efgsfo  18152  ablfaclem3  18486  ringpropd  18582  islmodd  18869  lmodprop2d  18925  lss1d  18963  assamulgscmlem2  19349  mplcoe1  19465  mplcoe5  19468  evlslem1  19515  lindff1  20159  islindf4  20177  mdetunilem7  20424  mdetunilem8  20425  mdetunilem9  20426  mdetuni0  20427  mdetmul  20429  ppttop  20811  epttop  20813  cnhaus  21158  isreg2  21181  cncmp  21195  1stcfb  21248  2ndcomap  21261  cldllycmp  21298  txcls  21407  ptclsg  21418  ptcnp  21425  txdis1cn  21438  txlly  21439  txnlly  21440  pthaus  21441  txhaus  21450  txkgen  21455  xkohaus  21456  xkococnlem  21462  xkococn  21463  fgabs  21683  rnelfm  21757  hausflimi  21784  hausflim  21785  alexsubALTlem2  21852  alexsubALTlem4  21854  alexsubALT  21855  tgpconncomp  21916  qustgplem  21924  metequiv2  22315  met2ndci  22327  nrmmetd  22379  nlmvscnlem1  22490  reconn  22631  xrge0tsms  22637  ipcnlem1  23044  minveclem3  23200  pmltpc  23219  ovolicc2lem5  23289  ovolicc2  23290  uniioombllem6  23356  dyadmbllem  23367  vitalilem3  23379  mbfmullem  23492  itg2split  23516  itg2mono  23520  dvlip2  23758  lhop1  23777  dvcnvrelem1  23780  ftc1lem6  23804  itgsubst  23812  dgrco  24031  plyexmo  24068  ulmdvlem3  24156  abelthlem2  24186  abelthlem8  24193  dvdsmulf1o  24920  chpchtsum  24944  dchrptlem2  24990  2sqlem5  25147  2sqlem9  25152  2sqb  25157  pntrlog2bnd  25273  pntibndlem3  25281  pntlemp  25299  pnt3  25301  hlcgreu  25513  mirreu3  25549  cgraswap  25712  cgracom  25714  cgratr  25715  acopyeu  25725  axsegcon  25807  ax5seglem9  25817  axeuclid  25843  axcontlem12  25855  clwwlksf1  26917  wwlksext2clwwlk  26924  frgrnbnb  27157  ablo4  27404  smcnlem  27552  pjhthmo  28161  pjpjpre  28278  3oalem2  28522  lnconi  28892  atom1d  29212  resf1o  29505  xrge0tsmsd  29785  ballotlemfc0  30554  ballotlemfcc  30555  pconnconn  31213  cvmfolem  31261  cvmliftmo  31266  cvmliftlem7  31273  cvmlift2lem10  31294  cvmlift3lem8  31308  noresle  31846  lineext  32183  linecgr  32188  btwnconn1lem10  32203  btwnconn1lem11  32204  btwnconn3  32210  brsegle  32215  seglecgr12im  32217  segleantisym  32222  outsideoftr  32236  outsideofeq  32237  outsideofeu  32238  linethru  32260  finminlem  32312  neibastop2lem  32355  isbasisrelowllem1  33203  isbasisrelowllem2  33204  mblfinlem3  33448  bddiblnc  33480  ftc1cnnc  33484  isbnd3  33583  heibor1lem  33608  crngm4  33802  cvlcvr1  34626  4atlem12  34898  paddasslem12  35117  paddasslem13  35118  lhpexle2lem  35295  trlord  35857  cdlemkid4  36222  dihopelvalcpre  36537  dihmeetlem1N  36579  dihglblem5apreN  36580  dihmeetlem6  36598  dih1dimatlem0  36617  dihjatcclem4  36710  mzpcl2  37293  mzpmfp  37310  mzpcompact2lem  37314  diophin  37336  pell14qrmulcl  37427  hbtlem2  37694  iunrelexpuztr  38011  stoweidlem61  40278  fourierdlem92  40415  snlindsntor  42260  elfzolborelfzop1  42309  nn0sumshdiglemB  42414