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  7227  fliftfun  7252  fprresex  8246  domunfican  9212  finsschain  9249  suppeqfsuppbi  9269  fsuppunbi  9279  wemapsolem  9442  wemapso  9443  wemapso2lem  9444  cantnf  9589  enfin2i  10218  ttukeylem7  10412  fpwwe2lem2  10529  fpwwe2lem8  10535  fpwwe2lem11  10538  fpwwelem  10542  distrlem4pr  10923  mulcmpblnr  10968  prsrlem1  10969  addsrmo  10970  mulsrmo  10971  divdivdiv  11828  divsubdiv  11843  lediv12a  12021  xmullem  13169  xlemul1a  13193  seqcaopr  13952  leexp2r  14087  hashf1lem1  14368  hashf1lem2  14369  fi1uzind  14420  brfi1indALT  14423  wrd2ind  14636  swrdccat  14648  cshweqrep  14734  rtrclreclem4  14974  summolem2  15629  summo  15630  prodmolem2  15848  prodmo  15849  bezoutlem3  16458  bezoutlem4  16459  qredeu  16575  pcadd  16807  vdwlem9  16907  vdwlem10  16908  ramub1lem2  16945  ramub1  16946  cofucl  17801  setcmon  18000  poslubmo  18321  posglbmo  18322  grprcan  18892  isnsg3  19078  ghmpreima  19156  gaorber  19226  psgneu  19424  odcau  19522  lsmsubm  19571  lsmmod  19593  efgsfo  19657  ablfaclem3  20007  rngpropd  20098  ringpropd  20212  islmodd  20805  lmodprop2d  20863  lss1d  20902  lindff1  21763  islindf4  21781  assamulgscmlem2  21843  mplcoe1  21978  mplcoe5  21981  evlslem1  22023  mdetunilem7  22539  mdetunilem8  22540  mdetunilem9  22541  mdetuni0  22542  mdetmul  22544  ppttop  22928  epttop  22930  cnhaus  23275  isreg2  23298  cncmp  23313  1stcfb  23366  2ndcomap  23379  cldllycmp  23416  txcls  23525  ptclsg  23536  ptcnp  23543  txdis1cn  23556  txlly  23557  txnlly  23558  pthaus  23559  txhaus  23568  txkgen  23573  xkohaus  23574  xkococnlem  23580  xkococn  23581  fgabs  23800  rnelfm  23874  hausflimi  23901  hausflim  23902  alexsubALTlem2  23969  alexsubALTlem4  23971  alexsubALT  23972  tgpconncomp  24034  qustgplem  24042  metequiv2  24431  met2ndci  24443  nrmmetd  24495  nlmvscnlem1  24607  reconn  24750  xrge0tsms  24756  ipcnlem1  25178  minveclem3  25362  pmltpc  25384  ovolicc2lem5  25455  ovolicc2  25456  uniioombllem6  25522  dyadmbllem  25533  vitalilem3  25544  mbfmullem  25659  itg2split  25683  itg2mono  25687  bddiblnc  25776  dvlip2  25933  lhop1  25952  dvcnvrelem1  25955  ftc1lem6  25981  itgsubst  25989  dgrco  26214  plyexmo  26254  ulmdvlem3  26344  abelthlem2  26375  abelthlem8  26382  mpodvdsmulf1o  27137  dvdsmulf1o  27139  chpchtsum  27163  dchrptlem2  27209  2sqlem5  27366  2sqlem9  27371  2sqb  27376  pntrlog2bnd  27528  pntibndlem3  27536  pntlemp  27554  pnt3  27556  noresle  27642  nosupprefixmo  27645  noinfprefixmo  27646  addsprop  27925  mulsproplem9  28069  mulsasslem3  28110  onscutlt  28207  expadds  28364  readdscl  28407  tgjustf  28457  hlcgreu  28602  mirreu3  28638  cgraswap  28804  cgracom  28806  cgratr  28807  flatcgra  28808  acopyeu  28818  axsegcon  28912  ax5seglem9  28922  axeuclid  28948  axcontlem12  28960  clwwlkf1  30036  n4cyclfrgr  30278  frgrnbnb  30280  ablo4  30537  smcnlem  30684  pjhthmo  31289  pjpjpre  31406  3oalem2  31650  lnconi  32020  atom1d  32340  resf1o  32720  mgcoval  32974  xrge0tsmsd  33049  erlval  33232  ballotlemfc0  34513  ballotlemfcc  34514  pconnconn  35282  cvmfolem  35330  cvmliftmo  35335  cvmliftlem7  35342  cvmlift2lem10  35363  cvmlift3lem8  35377  lineext  36127  linecgr  36132  btwnconn1lem10  36147  btwnconn1lem11  36148  btwnconn3  36154  brsegle  36159  seglecgr12im  36161  segleantisym  36166  outsideoftr  36180  outsideofeq  36181  outsideofeu  36182  linethru  36204  finminlem  36369  neibastop2lem  36411  weiunpo  36516  isbasisrelowllem1  37406  isbasisrelowllem2  37407  mblfinlem3  37705  ftc1cnnc  37738  isbnd3  37830  heibor1lem  37855  crngm4  38049  cvlcvr1  39444  4atlem12  39717  paddasslem12  39936  paddasslem13  39937  lhpexle2lem  40114  trlord  40674  cdlemkid4  41039  dihopelvalcpre  41353  dihmeetlem1N  41395  dihglblem5apreN  41396  dihmeetlem6  41414  dih1dimatlem0  41433  dihjatcclem4  41526  unitscyglem4  42297  prjspner1  42725  mzpcl2  42828  mzpmfp  42845  mzpcompact2lem  42849  diophin  42870  pell14qrmulcl  42961  hbtlem2  43222  iunrelexpuztr  43817  stoweidlem61  46164  fourierdlem92  46301  euoreqb  47214  prproropf1olem3  47610  prproropf1olem4  47611  fpprwpprb  47845  cycldlenngric  48033  grimgrtri  48054  snlindsntor  48577  elfzolborelfzop1  48625  nn0sumshdiglemB  48726  2arwcat  49706