Theorem simprlr 792

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 490	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrl 741	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fcof1  7291  fliftfun  7316  fprresex  8312  domunfican  9294  finsschain  9329  suppeqfsuppbi  9352  fsuppunbi  9362  wemapsolem  9525  wemapso  9526  wemapso2lem  9527  cantnf  9675  enfin2i  10326  ttukeylem7  10520  fpwwe2lem2  10644  fpwwe2lem8  10650  fpwwe2lem11  10653  fpwwelem  10657  distrlem4pr  11038  mulcmpblnr  11083  prsrlem1  11084  addsrmo  11085  mulsrmo  11086  divdivdiv  11943  divsubdiv  11958  lediv12a  12135  xmullem  13318  xlemul1a  13342  seqcaopr  14105  leexp2r  14240  hashf1lem1  14522  hashf1lem2  14523  fi1uzind  14574  brfi1indALT  14577  wrd2ind  14794  swrdccat  14806  cshweqrep  14894  rtrclreclem4  15136  summolem2  15804  summo  15805  prodmolem2  16026  prodmo  16027  bezoutlem3  16635  bezoutlem4  16636  qredeu  16752  pcadd  16985  vdwlem9  17085  vdwlem10  17086  ramub1lem2  17123  ramub1  17124  cofucl  17981  setcmon  18180  poslubmo  18501  posglbmo  18502  grprcan  19098  isnsg3  19284  ghmpreima  19366  gaorber  19436  psgneu  19634  odcau  19732  lsmsubm  19781  lsmmod  19803  efgsfo  19867  ablfaclem3  20217  rngpropd  20310  ringpropd  20431  islmodd  21051  lmodprop2d  21109  lss1d  21148  lindff1  22034  islindf4  22052  assamulgscmlem2  22116  mplcoe1  22254  mplcoe5  22257  evlslem1  22299  mdetunilem7  22841  mdetunilem8  22842  mdetunilem9  22843  mdetuni0  22844  mdetmul  22846  ppttop  23233  epttop  23235  cnhaus  23580  isreg2  23603  cncmp  23618  1stcfb  23671  2ndcomap  23685  cldllycmp  23722  txcls  23831  ptclsg  23842  ptcnp  23849  txdis1cn  23862  txlly  23863  txnlly  23864  pthaus  23865  txhaus  23874  txkgen  23879  xkohaus  23880  xkococnlem  23886  xkococn  23887  fgabs  24106  rnelfm  24180  hausflimi  24207  hausflim  24208  alexsubALTlem2  24275  alexsubALTlem4  24277  alexsubALT  24278  tgpconncomp  24340  qustgplem  24348  metequiv2  24737  met2ndci  24749  nrmmetd  24801  nlmvscnlem1  24913  reconn  25056  xrge0tsms  25062  ipcnlem1  25474  minveclem3  25658  pmltpc  25679  ovolicc2lem5  25750  ovolicc2  25751  uniioombllem6  25817  dyadmbllem  25828  vitalilem3  25839  mbfmullem  25954  itg2split  25978  itg2mono  25982  bddiblnc  26071  dvlip2  26224  lhop1  26243  dvcnvrelem1  26246  ftc1lem6  26270  itgsubst  26278  dgrco  26502  plyexmo  26544  ulmdvlem3  26635  abelthlem2  26665  abelthlem8  26672  mpodvdsmulf1o  27428  dvdsmulf1o  27430  chpchtsum  27453  dchrptlem2  27499  2sqlem5  27656  2sqlem9  27661  2sqb  27666  pntrlog2bnd  27818  pntibndlem3  27826  pntlemp  27844  pnt3  27846  noresle  27931  nosupprefixmo  27934  noinfprefixmo  27935  addsprop  28239  mulsproplem9  28387  mulsasslem3  28428  oncutlt  28527  expadds  28698  bdayfinbndlem1  28730  readdscl  28762  tgjustf  28812  hlcgreu  28961  mirreu3  29003  cgraswap  29204  cgracom  29206  cgratr  29207  flatcgra  29209  acopyeu  29219  brprlng  29281  axsegcon  29370  ax5seglem9  29380  axeuclid  29406  axcontlem12  29418  clwwlkf1  30505  n4cyclfrgr  30757  frgrnbnb  30759  ablo4  31017  smcnlem  31164  pjhthmo  31769  pjpjpre  31886  3oalem2  32130  lnconi  32500  atom1d  32820  resf1o  33188  mgcoval  33413  xrge0tsmsd  33500  erlval  33685  ballotlemfc0  34991  ballotlemfcc  34992  pconnconn  35797  cvmfolem  35845  cvmliftmo  35850  cvmliftlem7  35857  cvmlift2lem10  35878  cvmlift3lem8  35892  lineext  36643  linecgr  36648  btwnconn1lem10  36663  btwnconn1lem11  36664  btwnconn3  36670  brsegle  36675  seglecgr12im  36677  segleantisym  36682  outsideoftr  36696  outsideofeq  36697  outsideofeu  36698  linethru  36720  nadddilem1  36787  finminlem  36924  neibastop2lem  36966  weiunpo  37071  isbasisrelowllem1  38096  isbasisrelowllem2  38097  mblfinlem3  38395  ftc1cnnc  38428  isbnd3  38521  heibor1lem  38546  crngm4  38740  cvlcvr1  40199  4atlem12  40472  paddasslem12  40691  paddasslem13  40692  lhpexle2lem  40869  trlord  41429  cdlemkid4  41794  dihopelvalcpre  42108  dihmeetlem1N  42150  dihglblem5apreN  42151  dihmeetlem6  42169  dih1dimatlem0  42188  dihjatcclem4  42281  unitscyglem4  43051  prjspner1  43459  mzpcl2  43562  mzpmfp  43579  mzpcompact2lem  43583  diophin  43604  pell14qrmulcl  43691  hbtlem2  43952  iunrelexpuztr  44546  stoweidlem61  46876  fourierdlem92  47013  euoreqb  47984  prproropf1olem3  48392  prproropf1olem4  48393  fpprwpprb  48643  cycldlenngric  48831  grimgrtri  48852  snlindsntor  49388  elfzolborelfzop1  49436  nn0sumshdiglemB  49537  2arwcat  50513