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  7262  fliftfun  7287  fprresex  8289  domunfican  9272  finsschain  9310  suppeqfsuppbi  9330  fsuppunbi  9340  wemapsolem  9503  wemapso  9504  wemapso2lem  9505  cantnf  9646  enfin2i  10274  ttukeylem7  10468  fpwwe2lem2  10585  fpwwe2lem8  10591  fpwwe2lem11  10594  fpwwelem  10598  distrlem4pr  10979  mulcmpblnr  11024  prsrlem1  11025  addsrmo  11026  mulsrmo  11027  divdivdiv  11883  divsubdiv  11898  lediv12a  12076  xmullem  13224  xlemul1a  13248  seqcaopr  14004  leexp2r  14139  hashf1lem1  14420  hashf1lem2  14421  fi1uzind  14472  brfi1indALT  14475  wrd2ind  14688  swrdccat  14700  cshweqrep  14786  rtrclreclem4  15027  summolem2  15682  summo  15683  prodmolem2  15901  prodmo  15902  bezoutlem3  16511  bezoutlem4  16512  qredeu  16628  pcadd  16860  vdwlem9  16960  vdwlem10  16961  ramub1lem2  16998  ramub1  16999  cofucl  17850  setcmon  18049  poslubmo  18370  posglbmo  18371  grprcan  18905  isnsg3  19092  ghmpreima  19170  gaorber  19240  psgneu  19436  odcau  19534  lsmsubm  19583  lsmmod  19605  efgsfo  19669  ablfaclem3  20019  rngpropd  20083  ringpropd  20197  islmodd  20772  lmodprop2d  20830  lss1d  20869  lindff1  21729  islindf4  21747  assamulgscmlem2  21809  mplcoe1  21944  mplcoe5  21947  evlslem1  21989  mdetunilem7  22505  mdetunilem8  22506  mdetunilem9  22507  mdetuni0  22508  mdetmul  22510  ppttop  22894  epttop  22896  cnhaus  23241  isreg2  23264  cncmp  23279  1stcfb  23332  2ndcomap  23345  cldllycmp  23382  txcls  23491  ptclsg  23502  ptcnp  23509  txdis1cn  23522  txlly  23523  txnlly  23524  pthaus  23525  txhaus  23534  txkgen  23539  xkohaus  23540  xkococnlem  23546  xkococn  23547  fgabs  23766  rnelfm  23840  hausflimi  23867  hausflim  23868  alexsubALTlem2  23935  alexsubALTlem4  23937  alexsubALT  23938  tgpconncomp  24000  qustgplem  24008  metequiv2  24398  met2ndci  24410  nrmmetd  24462  nlmvscnlem1  24574  reconn  24717  xrge0tsms  24723  ipcnlem1  25145  minveclem3  25329  pmltpc  25351  ovolicc2lem5  25422  ovolicc2  25423  uniioombllem6  25489  dyadmbllem  25500  vitalilem3  25511  mbfmullem  25626  itg2split  25650  itg2mono  25654  bddiblnc  25743  dvlip2  25900  lhop1  25919  dvcnvrelem1  25922  ftc1lem6  25948  itgsubst  25956  dgrco  26181  plyexmo  26221  ulmdvlem3  26311  abelthlem2  26342  abelthlem8  26349  mpodvdsmulf1o  27104  dvdsmulf1o  27106  chpchtsum  27130  dchrptlem2  27176  2sqlem5  27333  2sqlem9  27338  2sqb  27343  pntrlog2bnd  27495  pntibndlem3  27503  pntlemp  27521  pnt3  27523  noresle  27609  nosupprefixmo  27612  noinfprefixmo  27613  addsprop  27883  mulsproplem9  28027  mulsasslem3  28068  onscutlt  28165  expadds  28320  readdscl  28350  tgjustf  28400  hlcgreu  28545  mirreu3  28581  cgraswap  28747  cgracom  28749  cgratr  28750  flatcgra  28751  acopyeu  28761  axsegcon  28854  ax5seglem9  28864  axeuclid  28890  axcontlem12  28902  clwwlkf1  29978  n4cyclfrgr  30220  frgrnbnb  30222  ablo4  30479  smcnlem  30626  pjhthmo  31231  pjpjpre  31348  3oalem2  31592  lnconi  31962  atom1d  32282  resf1o  32653  mgcoval  32912  xrge0tsmsd  33002  erlval  33209  ballotlemfc0  34484  ballotlemfcc  34485  pconnconn  35218  cvmfolem  35266  cvmliftmo  35271  cvmliftlem7  35278  cvmlift2lem10  35299  cvmlift3lem8  35313  lineext  36064  linecgr  36069  btwnconn1lem10  36084  btwnconn1lem11  36085  btwnconn3  36091  brsegle  36096  seglecgr12im  36098  segleantisym  36103  outsideoftr  36117  outsideofeq  36118  outsideofeu  36119  linethru  36141  finminlem  36306  neibastop2lem  36348  weiunpo  36453  isbasisrelowllem1  37343  isbasisrelowllem2  37344  mblfinlem3  37653  ftc1cnnc  37686  isbnd3  37778  heibor1lem  37803  crngm4  37997  cvlcvr1  39332  4atlem12  39606  paddasslem12  39825  paddasslem13  39826  lhpexle2lem  40003  trlord  40563  cdlemkid4  40928  dihopelvalcpre  41242  dihmeetlem1N  41284  dihglblem5apreN  41285  dihmeetlem6  41303  dih1dimatlem0  41322  dihjatcclem4  41415  unitscyglem4  42186  prjspner1  42614  mzpcl2  42718  mzpmfp  42735  mzpcompact2lem  42739  diophin  42760  pell14qrmulcl  42851  hbtlem2  43113  iunrelexpuztr  43708  stoweidlem61  46059  fourierdlem92  46196  euoreqb  47110  prproropf1olem3  47506  prproropf1olem4  47507  fpprwpprb  47741  cycldlenngric  47928  grimgrtri  47948  snlindsntor  48460  elfzolborelfzop1  48508  nn0sumshdiglemB  48609  2arwcat  49589