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  7216  fliftfun  7241  fprresex  8235  domunfican  9201  finsschain  9238  suppeqfsuppbi  9258  fsuppunbi  9268  wemapsolem  9431  wemapso  9432  wemapso2lem  9433  cantnf  9578  enfin2i  10204  ttukeylem7  10398  fpwwe2lem2  10515  fpwwe2lem8  10521  fpwwe2lem11  10524  fpwwelem  10528  distrlem4pr  10909  mulcmpblnr  10954  prsrlem1  10955  addsrmo  10956  mulsrmo  10957  divdivdiv  11814  divsubdiv  11829  lediv12a  12007  xmullem  13155  xlemul1a  13179  seqcaopr  13938  leexp2r  14073  hashf1lem1  14354  hashf1lem2  14355  fi1uzind  14406  brfi1indALT  14409  wrd2ind  14622  swrdccat  14634  cshweqrep  14720  rtrclreclem4  14960  summolem2  15615  summo  15616  prodmolem2  15834  prodmo  15835  bezoutlem3  16444  bezoutlem4  16445  qredeu  16561  pcadd  16793  vdwlem9  16893  vdwlem10  16894  ramub1lem2  16931  ramub1  16932  cofucl  17787  setcmon  17986  poslubmo  18307  posglbmo  18308  grprcan  18878  isnsg3  19065  ghmpreima  19143  gaorber  19213  psgneu  19411  odcau  19509  lsmsubm  19558  lsmmod  19580  efgsfo  19644  ablfaclem3  19994  rngpropd  20085  ringpropd  20199  islmodd  20792  lmodprop2d  20850  lss1d  20889  lindff1  21750  islindf4  21768  assamulgscmlem2  21830  mplcoe1  21965  mplcoe5  21968  evlslem1  22010  mdetunilem7  22526  mdetunilem8  22527  mdetunilem9  22528  mdetuni0  22529  mdetmul  22531  ppttop  22915  epttop  22917  cnhaus  23262  isreg2  23285  cncmp  23300  1stcfb  23353  2ndcomap  23366  cldllycmp  23403  txcls  23512  ptclsg  23523  ptcnp  23530  txdis1cn  23543  txlly  23544  txnlly  23545  pthaus  23546  txhaus  23555  txkgen  23560  xkohaus  23561  xkococnlem  23567  xkococn  23568  fgabs  23787  rnelfm  23861  hausflimi  23888  hausflim  23889  alexsubALTlem2  23956  alexsubALTlem4  23958  alexsubALT  23959  tgpconncomp  24021  qustgplem  24029  metequiv2  24418  met2ndci  24430  nrmmetd  24482  nlmvscnlem1  24594  reconn  24737  xrge0tsms  24743  ipcnlem1  25165  minveclem3  25349  pmltpc  25371  ovolicc2lem5  25442  ovolicc2  25443  uniioombllem6  25509  dyadmbllem  25520  vitalilem3  25531  mbfmullem  25646  itg2split  25670  itg2mono  25674  bddiblnc  25763  dvlip2  25920  lhop1  25939  dvcnvrelem1  25942  ftc1lem6  25968  itgsubst  25976  dgrco  26201  plyexmo  26241  ulmdvlem3  26331  abelthlem2  26362  abelthlem8  26369  mpodvdsmulf1o  27124  dvdsmulf1o  27126  chpchtsum  27150  dchrptlem2  27196  2sqlem5  27353  2sqlem9  27358  2sqb  27363  pntrlog2bnd  27515  pntibndlem3  27523  pntlemp  27541  pnt3  27543  noresle  27629  nosupprefixmo  27632  noinfprefixmo  27633  addsprop  27912  mulsproplem9  28056  mulsasslem3  28097  onscutlt  28194  expadds  28351  readdscl  28394  tgjustf  28444  hlcgreu  28589  mirreu3  28625  cgraswap  28791  cgracom  28793  cgratr  28794  flatcgra  28795  acopyeu  28805  axsegcon  28898  ax5seglem9  28908  axeuclid  28934  axcontlem12  28946  clwwlkf1  30019  n4cyclfrgr  30261  frgrnbnb  30263  ablo4  30520  smcnlem  30667  pjhthmo  31272  pjpjpre  31389  3oalem2  31633  lnconi  32003  atom1d  32323  resf1o  32703  mgcoval  32957  xrge0tsmsd  33032  erlval  33215  ballotlemfc0  34496  ballotlemfcc  34497  pconnconn  35243  cvmfolem  35291  cvmliftmo  35296  cvmliftlem7  35303  cvmlift2lem10  35324  cvmlift3lem8  35338  lineext  36089  linecgr  36094  btwnconn1lem10  36109  btwnconn1lem11  36110  btwnconn3  36116  brsegle  36121  seglecgr12im  36123  segleantisym  36128  outsideoftr  36142  outsideofeq  36143  outsideofeu  36144  linethru  36166  finminlem  36331  neibastop2lem  36373  weiunpo  36478  isbasisrelowllem1  37368  isbasisrelowllem2  37369  mblfinlem3  37678  ftc1cnnc  37711  isbnd3  37803  heibor1lem  37828  crngm4  38022  cvlcvr1  39357  4atlem12  39630  paddasslem12  39849  paddasslem13  39850  lhpexle2lem  40027  trlord  40587  cdlemkid4  40952  dihopelvalcpre  41266  dihmeetlem1N  41308  dihglblem5apreN  41309  dihmeetlem6  41327  dih1dimatlem0  41346  dihjatcclem4  41439  unitscyglem4  42210  prjspner1  42638  mzpcl2  42742  mzpmfp  42759  mzpcompact2lem  42763  diophin  42784  pell14qrmulcl  42875  hbtlem2  43136  iunrelexpuztr  43731  stoweidlem61  46078  fourierdlem92  46215  euoreqb  47119  prproropf1olem3  47515  prproropf1olem4  47516  fpprwpprb  47750  cycldlenngric  47938  grimgrtri  47959  snlindsntor  48482  elfzolborelfzop1  48530  nn0sumshdiglemB  48631  2arwcat  49611