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 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  7306  fliftfun  7331  fprresex  8333  wfrlem17OLD  8363  domunfican  9358  finsschain  9396  suppeqfsuppbi  9416  fsuppunbi  9426  wemapsolem  9587  wemapso  9588  wemapso2lem  9589  cantnf  9730  enfin2i  10358  ttukeylem7  10552  fpwwe2lem2  10669  fpwwe2lem8  10675  fpwwe2lem11  10678  fpwwelem  10682  distrlem4pr  11063  mulcmpblnr  11108  prsrlem1  11109  addsrmo  11110  mulsrmo  11111  divdivdiv  11965  divsubdiv  11980  lediv12a  12158  xmullem  13302  xlemul1a  13326  seqcaopr  14076  leexp2r  14210  hashf1lem1  14490  hashf1lem2  14491  fi1uzind  14542  brfi1indALT  14545  wrd2ind  14757  swrdccat  14769  cshweqrep  14855  rtrclreclem4  15096  summolem2  15748  summo  15749  prodmolem2  15967  prodmo  15968  bezoutlem3  16574  bezoutlem4  16575  qredeu  16691  pcadd  16922  vdwlem9  17022  vdwlem10  17023  ramub1lem2  17060  ramub1  17061  cofucl  17938  setcmon  18140  poslubmo  18468  posglbmo  18469  grprcan  19003  isnsg3  19190  ghmpreima  19268  gaorber  19338  psgneu  19538  odcau  19636  lsmsubm  19685  lsmmod  19707  efgsfo  19771  ablfaclem3  20121  rngpropd  20191  ringpropd  20301  islmodd  20880  lmodprop2d  20938  lss1d  20978  lindff1  21857  islindf4  21875  assamulgscmlem2  21937  mplcoe1  22072  mplcoe5  22075  evlslem1  22123  mdetunilem7  22639  mdetunilem8  22640  mdetunilem9  22641  mdetuni0  22642  mdetmul  22644  ppttop  23029  epttop  23031  cnhaus  23377  isreg2  23400  cncmp  23415  1stcfb  23468  2ndcomap  23481  cldllycmp  23518  txcls  23627  ptclsg  23638  ptcnp  23645  txdis1cn  23658  txlly  23659  txnlly  23660  pthaus  23661  txhaus  23670  txkgen  23675  xkohaus  23676  xkococnlem  23682  xkococn  23683  fgabs  23902  rnelfm  23976  hausflimi  24003  hausflim  24004  alexsubALTlem2  24071  alexsubALTlem4  24073  alexsubALT  24074  tgpconncomp  24136  qustgplem  24144  metequiv2  24538  met2ndci  24550  nrmmetd  24602  nlmvscnlem1  24722  reconn  24863  xrge0tsms  24869  ipcnlem1  25292  minveclem3  25476  pmltpc  25498  ovolicc2lem5  25569  ovolicc2  25570  uniioombllem6  25636  dyadmbllem  25647  vitalilem3  25658  mbfmullem  25774  itg2split  25798  itg2mono  25802  bddiblnc  25891  dvlip2  26048  lhop1  26067  dvcnvrelem1  26070  ftc1lem6  26096  itgsubst  26104  dgrco  26329  plyexmo  26369  ulmdvlem3  26459  abelthlem2  26490  abelthlem8  26497  mpodvdsmulf1o  27251  dvdsmulf1o  27253  chpchtsum  27277  dchrptlem2  27323  2sqlem5  27480  2sqlem9  27485  2sqb  27490  pntrlog2bnd  27642  pntibndlem3  27650  pntlemp  27668  pnt3  27670  noresle  27756  nosupprefixmo  27759  noinfprefixmo  27760  addsprop  28023  mulsproplem9  28164  mulsasslem3  28205  readdscl  28445  tgjustf  28495  hlcgreu  28640  mirreu3  28676  cgraswap  28842  cgracom  28844  cgratr  28845  flatcgra  28846  acopyeu  28856  axsegcon  28956  ax5seglem9  28966  axeuclid  28992  axcontlem12  29004  clwwlkf1  30077  n4cyclfrgr  30319  frgrnbnb  30321  ablo4  30578  smcnlem  30725  pjhthmo  31330  pjpjpre  31447  3oalem2  31691  lnconi  32061  atom1d  32381  resf1o  32747  mgcoval  32960  xrge0tsmsd  33047  erlval  33244  ballotlemfc0  34473  ballotlemfcc  34474  pconnconn  35215  cvmfolem  35263  cvmliftmo  35268  cvmliftlem7  35275  cvmlift2lem10  35296  cvmlift3lem8  35310  lineext  36057  linecgr  36062  btwnconn1lem10  36077  btwnconn1lem11  36078  btwnconn3  36084  brsegle  36089  seglecgr12im  36091  segleantisym  36096  outsideoftr  36110  outsideofeq  36111  outsideofeu  36112  linethru  36134  finminlem  36300  neibastop2lem  36342  weiunpo  36447  isbasisrelowllem1  37337  isbasisrelowllem2  37338  mblfinlem3  37645  ftc1cnnc  37678  isbnd3  37770  heibor1lem  37795  crngm4  37989  cvlcvr1  39320  4atlem12  39594  paddasslem12  39813  paddasslem13  39814  lhpexle2lem  39991  trlord  40551  cdlemkid4  40916  dihopelvalcpre  41230  dihmeetlem1N  41272  dihglblem5apreN  41273  dihmeetlem6  41291  dih1dimatlem0  41310  dihjatcclem4  41403  unitscyglem4  42179  prjspner1  42612  mzpcl2  42717  mzpmfp  42734  mzpcompact2lem  42738  diophin  42759  pell14qrmulcl  42850  hbtlem2  43112  iunrelexpuztr  43708  stoweidlem61  46016  fourierdlem92  46153  euoreqb  47058  prproropf1olem3  47429  prproropf1olem4  47430  fpprwpprb  47664  grimgrtri  47851  snlindsntor  48316  elfzolborelfzop1  48364  nn0sumshdiglemB  48469