Theorem simprlr 780

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 729	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  7235  fliftfun  7260  fprresex  8254  domunfican  9226  finsschain  9263  suppeqfsuppbi  9286  fsuppunbi  9296  wemapsolem  9459  wemapso  9460  wemapso2lem  9461  cantnf  9606  enfin2i  10235  ttukeylem7  10429  fpwwe2lem2  10547  fpwwe2lem8  10553  fpwwe2lem11  10556  fpwwelem  10560  distrlem4pr  10941  mulcmpblnr  10986  prsrlem1  10987  addsrmo  10988  mulsrmo  10989  divdivdiv  11846  divsubdiv  11861  lediv12a  12039  xmullem  13183  xlemul1a  13207  seqcaopr  13966  leexp2r  14101  hashf1lem1  14382  hashf1lem2  14383  fi1uzind  14434  brfi1indALT  14437  wrd2ind  14650  swrdccat  14662  cshweqrep  14748  rtrclreclem4  14988  summolem2  15643  summo  15644  prodmolem2  15862  prodmo  15863  bezoutlem3  16472  bezoutlem4  16473  qredeu  16589  pcadd  16821  vdwlem9  16921  vdwlem10  16922  ramub1lem2  16959  ramub1  16960  cofucl  17816  setcmon  18015  poslubmo  18336  posglbmo  18337  grprcan  18907  isnsg3  19093  ghmpreima  19171  gaorber  19241  psgneu  19439  odcau  19537  lsmsubm  19586  lsmmod  19608  efgsfo  19672  ablfaclem3  20022  rngpropd  20113  ringpropd  20227  islmodd  20821  lmodprop2d  20879  lss1d  20918  lindff1  21779  islindf4  21797  assamulgscmlem2  21860  mplcoe1  21996  mplcoe5  21999  evlslem1  22041  mdetunilem7  22566  mdetunilem8  22567  mdetunilem9  22568  mdetuni0  22569  mdetmul  22571  ppttop  22955  epttop  22957  cnhaus  23302  isreg2  23325  cncmp  23340  1stcfb  23393  2ndcomap  23406  cldllycmp  23443  txcls  23552  ptclsg  23563  ptcnp  23570  txdis1cn  23583  txlly  23584  txnlly  23585  pthaus  23586  txhaus  23595  txkgen  23600  xkohaus  23601  xkococnlem  23607  xkococn  23608  fgabs  23827  rnelfm  23901  hausflimi  23928  hausflim  23929  alexsubALTlem2  23996  alexsubALTlem4  23998  alexsubALT  23999  tgpconncomp  24061  qustgplem  24069  metequiv2  24458  met2ndci  24470  nrmmetd  24522  nlmvscnlem1  24634  reconn  24777  xrge0tsms  24783  ipcnlem1  25205  minveclem3  25389  pmltpc  25411  ovolicc2lem5  25482  ovolicc2  25483  uniioombllem6  25549  dyadmbllem  25560  vitalilem3  25571  mbfmullem  25686  itg2split  25710  itg2mono  25714  bddiblnc  25803  dvlip2  25960  lhop1  25979  dvcnvrelem1  25982  ftc1lem6  26008  itgsubst  26016  dgrco  26241  plyexmo  26281  ulmdvlem3  26371  abelthlem2  26402  abelthlem8  26409  mpodvdsmulf1o  27164  dvdsmulf1o  27166  chpchtsum  27190  dchrptlem2  27236  2sqlem5  27393  2sqlem9  27398  2sqb  27403  pntrlog2bnd  27555  pntibndlem3  27563  pntlemp  27581  pnt3  27583  noresle  27669  nosupprefixmo  27672  noinfprefixmo  27673  addsprop  27958  mulsproplem9  28106  mulsasslem3  28147  onscutlt  28245  expadds  28414  bdayfinbndlem1  28446  readdscl  28478  tgjustf  28528  hlcgreu  28673  mirreu3  28709  cgraswap  28875  cgracom  28877  cgratr  28878  flatcgra  28879  acopyeu  28889  axsegcon  28983  ax5seglem9  28993  axeuclid  29019  axcontlem12  29031  clwwlkf1  30107  n4cyclfrgr  30349  frgrnbnb  30351  ablo4  30608  smcnlem  30755  pjhthmo  31360  pjpjpre  31477  3oalem2  31721  lnconi  32091  atom1d  32411  resf1o  32790  mgcoval  33049  xrge0tsmsd  33136  erlval  33321  ballotlemfc0  34631  ballotlemfcc  34632  pconnconn  35406  cvmfolem  35454  cvmliftmo  35459  cvmliftlem7  35466  cvmlift2lem10  35487  cvmlift3lem8  35501  lineext  36251  linecgr  36256  btwnconn1lem10  36271  btwnconn1lem11  36272  btwnconn3  36278  brsegle  36283  seglecgr12im  36285  segleantisym  36290  outsideoftr  36304  outsideofeq  36305  outsideofeu  36306  linethru  36328  finminlem  36493  neibastop2lem  36535  weiunpo  36640  isbasisrelowllem1  37531  isbasisrelowllem2  37532  mblfinlem3  37831  ftc1cnnc  37864  isbnd3  37956  heibor1lem  37981  crngm4  38175  cvlcvr1  39636  4atlem12  39909  paddasslem12  40128  paddasslem13  40129  lhpexle2lem  40306  trlord  40866  cdlemkid4  41231  dihopelvalcpre  41545  dihmeetlem1N  41587  dihglblem5apreN  41588  dihmeetlem6  41606  dih1dimatlem0  41625  dihjatcclem4  41718  unitscyglem4  42489  prjspner1  42905  mzpcl2  43008  mzpmfp  43025  mzpcompact2lem  43029  diophin  43050  pell14qrmulcl  43141  hbtlem2  43402  iunrelexpuztr  43996  stoweidlem61  46341  fourierdlem92  46478  euoreqb  47391  prproropf1olem3  47787  prproropf1olem4  47788  fpprwpprb  48022  cycldlenngric  48210  grimgrtri  48231  snlindsntor  48753  elfzolborelfzop1  48801  nn0sumshdiglemB  48902  2arwcat  49881