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  7233  fliftfun  7258  fprresex  8251  domunfican  9223  finsschain  9260  suppeqfsuppbi  9283  fsuppunbi  9293  wemapsolem  9456  wemapso  9457  wemapso2lem  9458  cantnf  9603  enfin2i  10232  ttukeylem7  10426  fpwwe2lem2  10544  fpwwe2lem8  10550  fpwwe2lem11  10553  fpwwelem  10557  distrlem4pr  10938  mulcmpblnr  10983  prsrlem1  10984  addsrmo  10985  mulsrmo  10986  divdivdiv  11843  divsubdiv  11858  lediv12a  12036  xmullem  13180  xlemul1a  13204  seqcaopr  13963  leexp2r  14098  hashf1lem1  14379  hashf1lem2  14380  fi1uzind  14431  brfi1indALT  14434  wrd2ind  14647  swrdccat  14659  cshweqrep  14745  rtrclreclem4  14985  summolem2  15640  summo  15641  prodmolem2  15859  prodmo  15860  bezoutlem3  16469  bezoutlem4  16470  qredeu  16586  pcadd  16818  vdwlem9  16918  vdwlem10  16919  ramub1lem2  16956  ramub1  16957  cofucl  17813  setcmon  18012  poslubmo  18333  posglbmo  18334  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  20819  lmodprop2d  20877  lss1d  20916  lindff1  21777  islindf4  21795  assamulgscmlem2  21857  mplcoe1  21993  mplcoe5  21996  evlslem1  22038  mdetunilem7  22561  mdetunilem8  22562  mdetunilem9  22563  mdetuni0  22564  mdetmul  22566  ppttop  22950  epttop  22952  cnhaus  23297  isreg2  23320  cncmp  23335  1stcfb  23388  2ndcomap  23401  cldllycmp  23438  txcls  23547  ptclsg  23558  ptcnp  23565  txdis1cn  23578  txlly  23579  txnlly  23580  pthaus  23581  txhaus  23590  txkgen  23595  xkohaus  23596  xkococnlem  23602  xkococn  23603  fgabs  23822  rnelfm  23896  hausflimi  23923  hausflim  23924  alexsubALTlem2  23991  alexsubALTlem4  23993  alexsubALT  23994  tgpconncomp  24056  qustgplem  24064  metequiv2  24453  met2ndci  24465  nrmmetd  24517  nlmvscnlem1  24629  reconn  24772  xrge0tsms  24778  ipcnlem1  25190  minveclem3  25374  pmltpc  25395  ovolicc2lem5  25466  ovolicc2  25467  uniioombllem6  25533  dyadmbllem  25544  vitalilem3  25555  mbfmullem  25670  itg2split  25694  itg2mono  25698  bddiblnc  25787  dvlip2  25941  lhop1  25960  dvcnvrelem1  25963  ftc1lem6  25989  itgsubst  25997  dgrco  26221  plyexmo  26261  ulmdvlem3  26351  abelthlem2  26382  abelthlem8  26389  mpodvdsmulf1o  27144  dvdsmulf1o  27146  chpchtsum  27170  dchrptlem2  27216  2sqlem5  27373  2sqlem9  27378  2sqb  27383  pntrlog2bnd  27535  pntibndlem3  27543  pntlemp  27561  pnt3  27563  noresle  27649  nosupprefixmo  27652  noinfprefixmo  27653  addsprop  27956  mulsproplem9  28104  mulsasslem3  28145  oncutlt  28244  expadds  28415  bdayfinbndlem1  28447  readdscl  28479  tgjustf  28529  hlcgreu  28674  mirreu3  28710  cgraswap  28876  cgracom  28878  cgratr  28879  flatcgra  28880  acopyeu  28890  axsegcon  28984  ax5seglem9  28994  axeuclid  29020  axcontlem12  29032  clwwlkf1  30108  n4cyclfrgr  30350  frgrnbnb  30352  ablo4  30610  smcnlem  30757  pjhthmo  31362  pjpjpre  31479  3oalem2  31723  lnconi  32093  atom1d  32413  resf1o  32792  mgcoval  33051  xrge0tsmsd  33139  erlval  33324  ballotlemfc0  34643  ballotlemfcc  34644  pconnconn  35419  cvmfolem  35467  cvmliftmo  35472  cvmliftlem7  35479  cvmlift2lem10  35500  cvmlift3lem8  35514  lineext  36264  linecgr  36269  btwnconn1lem10  36284  btwnconn1lem11  36285  btwnconn3  36291  brsegle  36296  seglecgr12im  36298  segleantisym  36303  outsideoftr  36317  outsideofeq  36318  outsideofeu  36319  linethru  36341  finminlem  36506  neibastop2lem  36548  weiunpo  36653  isbasisrelowllem1  37667  isbasisrelowllem2  37668  mblfinlem3  37971  ftc1cnnc  38004  isbnd3  38096  heibor1lem  38121  crngm4  38315  cvlcvr1  39776  4atlem12  40049  paddasslem12  40268  paddasslem13  40269  lhpexle2lem  40446  trlord  41006  cdlemkid4  41371  dihopelvalcpre  41685  dihmeetlem1N  41727  dihglblem5apreN  41728  dihmeetlem6  41746  dih1dimatlem0  41765  dihjatcclem4  41858  unitscyglem4  42629  prjspner1  43058  mzpcl2  43161  mzpmfp  43178  mzpcompact2lem  43182  diophin  43203  pell14qrmulcl  43294  hbtlem2  43555  iunrelexpuztr  44149  stoweidlem61  46493  fourierdlem92  46630  euoreqb  47543  prproropf1olem3  47939  prproropf1olem4  47940  fpprwpprb  48174  cycldlenngric  48362  grimgrtri  48383  snlindsntor  48905  elfzolborelfzop1  48953  nn0sumshdiglemB  49054  2arwcat  50033