Theorem simprlr 799

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  disjxiunOLD  4580  fcof1  6442  fliftfun  6462  wfrlem17  7318  domunfican  8118  finsschain  8156  suppeqfsuppbi  8172  fsuppunbi  8179  wemapsolem  8338  wemapso  8339  wemapso2lem  8340  cantnf  8473  enfin2i  9026  ttukeylem7  9220  fpwwe2lem2  9333  fpwwe2lem9  9339  fpwwe2lem12  9342  fpwwelem  9346  distrlem4pr  9727  mulcmpblnr  9771  prsrlem1  9772  addsrmo  9773  mulsrmo  9774  divdivdiv  10605  divsubdiv  10620  lediv12a  10795  xmullem  11966  xlemul1a  11990  seqcaopr  12700  leexp2r  12780  hashf1lem1  13096  hashf1lem2  13097  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  wrd2ind  13329  cshweqrep  13418  summolem2  14294  summo  14295  prodmolem2  14504  prodmo  14505  bezoutlem3  15096  bezoutlem4  15097  qredeu  15210  pcadd  15431  vdwlem9  15531  vdwlem10  15532  ramub1lem2  15569  ramub1  15570  cofucl  16371  setcmon  16560  poslubmo  16969  posglbmo  16970  grprcan  17278  isnsg3  17451  ghmpreima  17505  gaorber  17564  psgneu  17749  odcau  17842  lsmsubm  17891  lsmmod  17911  efgsfo  17975  ablfaclem3  18309  ringpropd  18405  islmodd  18692  lmodprop2d  18748  lss1d  18784  assamulgscmlem2  19170  mplcoe1  19286  mplcoe5  19289  evlslem1  19336  lindff1  19978  islindf4  19996  mdetunilem7  20243  mdetunilem8  20244  mdetunilem9  20245  mdetuni0  20246  mdetmul  20248  ppttop  20621  epttop  20623  cnhaus  20968  isreg2  20991  cncmp  21005  1stcfb  21058  2ndcomap  21071  cldllycmp  21108  txcls  21217  ptclsg  21228  ptcnp  21235  txdis1cn  21248  txlly  21249  txnlly  21250  pthaus  21251  txhaus  21260  txkgen  21265  xkohaus  21266  xkococnlem  21272  xkococn  21273  fgabs  21493  rnelfm  21567  hausflimi  21594  hausflim  21595  alexsubALTlem2  21662  alexsubALTlem4  21664  alexsubALT  21665  tgpconcomp  21726  qustgplem  21734  metequiv2  22125  met2ndci  22137  nrmmetd  22189  nlmvscnlem1  22300  reconn  22439  xrge0tsms  22445  ipcnlem1  22852  minveclem3  23008  pmltpc  23026  ovolicc2lem5  23096  ovolicc2  23097  uniioombllem6  23162  dyadmbllem  23173  vitalilem3  23185  mbfmullem  23298  itg2split  23322  itg2mono  23326  dvlip2  23562  lhop1  23581  dvcnvrelem1  23584  ftc1lem6  23608  itgsubst  23616  dgrco  23835  plyexmo  23872  ulmdvlem3  23960  abelthlem2  23990  abelthlem8  23997  dvdsmulf1o  24720  chpchtsum  24744  dchrptlem2  24790  2sqlem5  24947  2sqlem9  24952  2sqb  24957  pntrlog2bnd  25073  pntibndlem3  25081  pntlemp  25099  pnt3  25101  hlcgreu  25313  mirreu3  25349  cgraswap  25512  cgracom  25514  cgratr  25515  acopyeu  25525  axsegcon  25607  ax5seglem9  25617  axeuclid  25643  axcontlem12  25655  clwwlkf1  26324  wwlkext2clwwlk  26331  frgranbnb  26547  ablo4  26788  smcnlem  26936  pjhthmo  27545  pjpjpre  27662  3oalem2  27906  lnconi  28276  atom1d  28596  resf1o  28893  xrge0tsmsd  29116  ballotlemfc0  29881  ballotlemfcc  29882  pconcon  30467  cvmfolem  30515  cvmliftmo  30520  cvmliftlem7  30527  cvmlift2lem10  30548  cvmlift3lem8  30562  lineext  31353  linecgr  31358  btwnconn1lem10  31373  btwnconn1lem11  31374  btwnconn3  31380  brsegle  31385  seglecgr12im  31387  segleantisym  31392  outsideoftr  31406  outsideofeq  31407  outsideofeu  31408  linethru  31430  finminlem  31482  neibastop2lem  31525  isbasisrelowllem1  32379  isbasisrelowllem2  32380  mblfinlem3  32618  bddiblnc  32650  ftc1cnnc  32654  isbnd3  32753  heibor1lem  32778  crngm4  32972  cvlcvr1  33644  4atlem12  33916  paddasslem12  34135  paddasslem13  34136  lhpexle2lem  34313  trlord  34875  cdlemkid4  35240  dihopelvalcpre  35555  dihmeetlem1N  35597  dihglblem5apreN  35598  dihmeetlem6  35616  dih1dimatlem0  35635  dihjatcclem4  35728  mzpcl2  36311  mzpmfp  36328  mzpcompact2lem  36332  diophin  36354  pell14qrmulcl  36445  hbtlem2  36713  iunrelexpuztr  37030  stoweidlem61  38954  fourierdlem92  39091  clwwlksf1  41224  wwlksext2clwwlk  41231  frgrnbnb  41463  snlindsntor  42054  elfzolborelfzop1  42103  nn0sumshdiglemB  42212