Theorem simprlr 789

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  fcof1  7271  fliftfun  7296  fprresex  8291  domunfican  9265  finsschain  9300  suppeqfsuppbi  9323  fsuppunbi  9333  wemapsolem  9496  wemapso  9497  wemapso2lem  9498  cantnf  9646  enfin2i  10289  ttukeylem7  10483  fpwwe2lem2  10601  fpwwe2lem8  10607  fpwwe2lem11  10610  fpwwelem  10614  distrlem4pr  10995  mulcmpblnr  11040  prsrlem1  11041  addsrmo  11042  mulsrmo  11043  divdivdiv  11903  divsubdiv  11918  lediv12a  12095  xmullem  13277  xlemul1a  13301  seqcaopr  14062  leexp2r  14197  hashf1lem1  14478  hashf1lem2  14479  fi1uzind  14530  brfi1indALT  14533  wrd2ind  14746  swrdccat  14758  cshweqrep  14844  rtrclreclem4  15084  summolem2  15753  summo  15754  prodmolem2  15975  prodmo  15976  bezoutlem3  16585  bezoutlem4  16586  qredeu  16702  pcadd  16935  vdwlem9  17035  vdwlem10  17036  ramub1lem2  17073  ramub1  17074  cofucl  17931  setcmon  18130  poslubmo  18451  posglbmo  18452  grprcan  19025  isnsg3  19211  ghmpreima  19288  gaorber  19358  psgneu  19556  odcau  19654  lsmsubm  19703  lsmmod  19725  efgsfo  19789  ablfaclem3  20139  rngpropd  20230  ringpropd  20348  islmodd  20940  lmodprop2d  20998  lss1d  21037  lindff1  21879  islindf4  21897  assamulgscmlem2  21959  mplcoe1  22097  mplcoe5  22100  evlslem1  22142  mdetunilem7  22685  mdetunilem8  22686  mdetunilem9  22687  mdetuni0  22688  mdetmul  22690  ppttop  23074  epttop  23076  cnhaus  23421  isreg2  23444  cncmp  23459  1stcfb  23512  2ndcomap  23525  cldllycmp  23562  txcls  23671  ptclsg  23682  ptcnp  23689  txdis1cn  23702  txlly  23703  txnlly  23704  pthaus  23705  txhaus  23714  txkgen  23719  xkohaus  23720  xkococnlem  23726  xkococn  23727  fgabs  23946  rnelfm  24020  hausflimi  24047  hausflim  24048  alexsubALTlem2  24115  alexsubALTlem4  24117  alexsubALT  24118  tgpconncomp  24180  qustgplem  24188  metequiv2  24577  met2ndci  24589  nrmmetd  24641  nlmvscnlem1  24753  reconn  24896  xrge0tsms  24902  ipcnlem1  25314  minveclem3  25498  pmltpc  25519  ovolicc2lem5  25590  ovolicc2  25591  uniioombllem6  25657  dyadmbllem  25668  vitalilem3  25679  mbfmullem  25794  itg2split  25818  itg2mono  25822  bddiblnc  25911  dvlip2  26064  lhop1  26083  dvcnvrelem1  26086  ftc1lem6  26110  itgsubst  26118  dgrco  26342  plyexmo  26384  ulmdvlem3  26472  abelthlem2  26502  abelthlem8  26509  mpodvdsmulf1o  27265  dvdsmulf1o  27267  chpchtsum  27290  dchrptlem2  27336  2sqlem5  27493  2sqlem9  27498  2sqb  27503  pntrlog2bnd  27655  pntibndlem3  27663  pntlemp  27681  pnt3  27683  noresle  27768  nosupprefixmo  27771  noinfprefixmo  27772  addsprop  28076  mulsproplem9  28224  mulsasslem3  28265  oncutlt  28364  expadds  28535  bdayfinbndlem1  28567  readdscl  28599  tgjustf  28649  hlcgreu  28794  mirreu3  28834  cgraswap  29021  cgracom  29023  cgratr  29024  flatcgra  29025  acopyeu  29035  brprlng  29072  axsegcon  29135  ax5seglem9  29145  axeuclid  29171  axcontlem12  29183  clwwlkf1  30258  n4cyclfrgr  30500  frgrnbnb  30502  ablo4  30760  smcnlem  30907  pjhthmo  31512  pjpjpre  31629  3oalem2  31873  lnconi  32243  atom1d  32563  resf1o  32938  mgcoval  33170  xrge0tsmsd  33259  erlval  33445  ballotlemfc0  34792  ballotlemfcc  34793  pconnconn  35586  cvmfolem  35634  cvmliftmo  35639  cvmliftlem7  35646  cvmlift2lem10  35667  cvmlift3lem8  35681  lineext  36431  linecgr  36436  btwnconn1lem10  36451  btwnconn1lem11  36452  btwnconn3  36458  brsegle  36463  seglecgr12im  36465  segleantisym  36470  outsideoftr  36484  outsideofeq  36485  outsideofeu  36486  linethru  36508  finminlem  36683  neibastop2lem  36725  weiunpo  36830  isbasisrelowllem1  37854  isbasisrelowllem2  37855  mblfinlem3  38163  ftc1cnnc  38196  isbnd3  38288  heibor1lem  38313  crngm4  38507  cvlcvr1  39968  4atlem12  40241  paddasslem12  40460  paddasslem13  40461  lhpexle2lem  40638  trlord  41198  cdlemkid4  41563  dihopelvalcpre  41877  dihmeetlem1N  41919  dihglblem5apreN  41920  dihmeetlem6  41938  dih1dimatlem0  41957  dihjatcclem4  42050  unitscyglem4  42820  prjspner1  43213  mzpcl2  43316  mzpmfp  43333  mzpcompact2lem  43337  diophin  43358  pell14qrmulcl  43445  hbtlem2  43706  iunrelexpuztr  44300  stoweidlem61  46626  fourierdlem92  46763  euoreqb  47694  prproropf1olem3  48102  prproropf1olem4  48103  fpprwpprb  48353  cycldlenngric  48541  grimgrtri  48562  snlindsntor  49084  elfzolborelfzop1  49132  nn0sumshdiglemB  49233  2arwcat  50212