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  7242  fliftfun  7267  fprresex  8260  domunfican  9232  finsschain  9269  suppeqfsuppbi  9292  fsuppunbi  9302  wemapsolem  9465  wemapso  9466  wemapso2lem  9467  cantnf  9614  enfin2i  10243  ttukeylem7  10437  fpwwe2lem2  10555  fpwwe2lem8  10561  fpwwe2lem11  10564  fpwwelem  10568  distrlem4pr  10949  mulcmpblnr  10994  prsrlem1  10995  addsrmo  10996  mulsrmo  10997  divdivdiv  11856  divsubdiv  11871  lediv12a  12049  xmullem  13216  xlemul1a  13240  seqcaopr  14001  leexp2r  14136  hashf1lem1  14417  hashf1lem2  14418  fi1uzind  14469  brfi1indALT  14472  wrd2ind  14685  swrdccat  14697  cshweqrep  14783  rtrclreclem4  15023  summolem2  15678  summo  15679  prodmolem2  15900  prodmo  15901  bezoutlem3  16510  bezoutlem4  16511  qredeu  16627  pcadd  16860  vdwlem9  16960  vdwlem10  16961  ramub1lem2  16998  ramub1  16999  cofucl  17855  setcmon  18054  poslubmo  18375  posglbmo  18376  grprcan  18949  isnsg3  19135  ghmpreima  19213  gaorber  19283  psgneu  19481  odcau  19579  lsmsubm  19628  lsmmod  19650  efgsfo  19714  ablfaclem3  20064  rngpropd  20155  ringpropd  20269  islmodd  20861  lmodprop2d  20919  lss1d  20958  lindff1  21800  islindf4  21818  assamulgscmlem2  21880  mplcoe1  22015  mplcoe5  22018  evlslem1  22060  mdetunilem7  22583  mdetunilem8  22584  mdetunilem9  22585  mdetuni0  22586  mdetmul  22588  ppttop  22972  epttop  22974  cnhaus  23319  isreg2  23342  cncmp  23357  1stcfb  23410  2ndcomap  23423  cldllycmp  23460  txcls  23569  ptclsg  23580  ptcnp  23587  txdis1cn  23600  txlly  23601  txnlly  23602  pthaus  23603  txhaus  23612  txkgen  23617  xkohaus  23618  xkococnlem  23624  xkococn  23625  fgabs  23844  rnelfm  23918  hausflimi  23945  hausflim  23946  alexsubALTlem2  24013  alexsubALTlem4  24015  alexsubALT  24016  tgpconncomp  24078  qustgplem  24086  metequiv2  24475  met2ndci  24487  nrmmetd  24539  nlmvscnlem1  24651  reconn  24794  xrge0tsms  24800  ipcnlem1  25212  minveclem3  25396  pmltpc  25417  ovolicc2lem5  25488  ovolicc2  25489  uniioombllem6  25555  dyadmbllem  25566  vitalilem3  25577  mbfmullem  25692  itg2split  25716  itg2mono  25720  bddiblnc  25809  dvlip2  25962  lhop1  25981  dvcnvrelem1  25984  ftc1lem6  26008  itgsubst  26016  dgrco  26240  plyexmo  26279  ulmdvlem3  26367  abelthlem2  26397  abelthlem8  26404  mpodvdsmulf1o  27157  dvdsmulf1o  27159  chpchtsum  27182  dchrptlem2  27228  2sqlem5  27385  2sqlem9  27390  2sqb  27395  pntrlog2bnd  27547  pntibndlem3  27555  pntlemp  27573  pnt3  27575  noresle  27661  nosupprefixmo  27664  noinfprefixmo  27665  addsprop  27968  mulsproplem9  28116  mulsasslem3  28157  oncutlt  28256  expadds  28427  bdayfinbndlem1  28459  readdscl  28491  tgjustf  28541  hlcgreu  28686  mirreu3  28722  cgraswap  28888  cgracom  28890  cgratr  28891  flatcgra  28892  acopyeu  28902  axsegcon  28996  ax5seglem9  29006  axeuclid  29032  axcontlem12  29044  clwwlkf1  30119  n4cyclfrgr  30361  frgrnbnb  30363  ablo4  30621  smcnlem  30768  pjhthmo  31373  pjpjpre  31490  3oalem2  31734  lnconi  32104  atom1d  32424  resf1o  32803  mgcoval  33046  xrge0tsmsd  33134  erlval  33319  ballotlemfc0  34637  ballotlemfcc  34638  pconnconn  35413  cvmfolem  35461  cvmliftmo  35466  cvmliftlem7  35473  cvmlift2lem10  35494  cvmlift3lem8  35508  lineext  36258  linecgr  36263  btwnconn1lem10  36278  btwnconn1lem11  36279  btwnconn3  36285  brsegle  36290  seglecgr12im  36292  segleantisym  36297  outsideoftr  36311  outsideofeq  36312  outsideofeu  36313  linethru  36335  finminlem  36500  neibastop2lem  36542  weiunpo  36647  isbasisrelowllem1  37671  isbasisrelowllem2  37672  mblfinlem3  37980  ftc1cnnc  38013  isbnd3  38105  heibor1lem  38130  crngm4  38324  cvlcvr1  39785  4atlem12  40058  paddasslem12  40277  paddasslem13  40278  lhpexle2lem  40455  trlord  41015  cdlemkid4  41380  dihopelvalcpre  41694  dihmeetlem1N  41736  dihglblem5apreN  41737  dihmeetlem6  41755  dih1dimatlem0  41774  dihjatcclem4  41867  unitscyglem4  42637  prjspner1  43059  mzpcl2  43162  mzpmfp  43179  mzpcompact2lem  43183  diophin  43204  pell14qrmulcl  43291  hbtlem2  43552  iunrelexpuztr  44146  stoweidlem61  46489  fourierdlem92  46626  euoreqb  47551  prproropf1olem3  47959  prproropf1olem4  47960  fpprwpprb  48210  cycldlenngric  48398  grimgrtri  48419  snlindsntor  48941  elfzolborelfzop1  48989  nn0sumshdiglemB  49090  2arwcat  50069