Theorem simprlr 777

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  fcof1  7168  fliftfun  7192  fprresex  8135  wfrlem17OLD  8165  domunfican  9096  finsschain  9135  suppeqfsuppbi  9151  fsuppunbi  9158  wemapsolem  9318  wemapso  9319  wemapso2lem  9320  cantnf  9460  enfin2i  10086  ttukeylem7  10280  fpwwe2lem2  10397  fpwwe2lem8  10403  fpwwe2lem11  10406  fpwwelem  10410  distrlem4pr  10791  mulcmpblnr  10836  prsrlem1  10837  addsrmo  10838  mulsrmo  10839  divdivdiv  11685  divsubdiv  11700  lediv12a  11877  xmullem  13007  xlemul1a  13031  seqcaopr  13769  leexp2r  13901  hashf1lem1  14177  hashf1lem1OLD  14178  hashf1lem2  14179  fi1uzind  14220  brfi1indALT  14223  wrd2ind  14445  swrdccat  14457  cshweqrep  14543  rtrclreclem4  14781  summolem2  15437  summo  15438  prodmolem2  15654  prodmo  15655  bezoutlem3  16258  bezoutlem4  16259  qredeu  16372  pcadd  16599  vdwlem9  16699  vdwlem10  16700  ramub1lem2  16737  ramub1  16738  cofucl  17612  setcmon  17811  poslubmo  18138  posglbmo  18139  grprcan  18622  isnsg3  18797  ghmpreima  18865  gaorber  18923  psgneu  19123  odcau  19218  lsmsubm  19267  lsmmod  19290  efgsfo  19354  ablfaclem3  19699  ringpropd  19830  islmodd  20138  lmodprop2d  20194  lss1d  20234  lindff1  21036  islindf4  21054  assamulgscmlem2  21113  mplcoe1  21247  mplcoe5  21250  evlslem1  21301  mdetunilem7  21776  mdetunilem8  21777  mdetunilem9  21778  mdetuni0  21779  mdetmul  21781  ppttop  22166  epttop  22168  cnhaus  22514  isreg2  22537  cncmp  22552  1stcfb  22605  2ndcomap  22618  cldllycmp  22655  txcls  22764  ptclsg  22775  ptcnp  22782  txdis1cn  22795  txlly  22796  txnlly  22797  pthaus  22798  txhaus  22807  txkgen  22812  xkohaus  22813  xkococnlem  22819  xkococn  22820  fgabs  23039  rnelfm  23113  hausflimi  23140  hausflim  23141  alexsubALTlem2  23208  alexsubALTlem4  23210  alexsubALT  23211  tgpconncomp  23273  qustgplem  23281  metequiv2  23675  met2ndci  23687  nrmmetd  23739  nlmvscnlem1  23859  reconn  24000  xrge0tsms  24006  ipcnlem1  24418  minveclem3  24602  pmltpc  24623  ovolicc2lem5  24694  ovolicc2  24695  uniioombllem6  24761  dyadmbllem  24772  vitalilem3  24783  mbfmullem  24899  itg2split  24923  itg2mono  24927  bddiblnc  25015  dvlip2  25168  lhop1  25187  dvcnvrelem1  25190  ftc1lem6  25214  itgsubst  25222  dgrco  25445  plyexmo  25482  ulmdvlem3  25570  abelthlem2  25600  abelthlem8  25607  dvdsmulf1o  26352  chpchtsum  26376  dchrptlem2  26422  2sqlem5  26579  2sqlem9  26584  2sqb  26589  pntrlog2bnd  26741  pntibndlem3  26749  pntlemp  26767  pnt3  26769  tgjustf  26843  hlcgreu  26988  mirreu3  27024  cgraswap  27190  cgracom  27192  cgratr  27193  flatcgra  27194  acopyeu  27204  axsegcon  27304  ax5seglem9  27314  axeuclid  27340  axcontlem12  27352  clwwlkf1  28422  n4cyclfrgr  28664  frgrnbnb  28666  ablo4  28921  smcnlem  29068  pjhthmo  29673  pjpjpre  29790  3oalem2  30034  lnconi  30404  atom1d  30724  resf1o  31074  mgcoval  31273  xrge0tsmsd  31326  ballotlemfc0  32468  ballotlemfcc  32469  pconnconn  33202  cvmfolem  33250  cvmliftmo  33255  cvmliftlem7  33262  cvmlift2lem10  33283  cvmlift3lem8  33297  noresle  33909  nosupprefixmo  33912  noinfprefixmo  33913  lineext  34387  linecgr  34392  btwnconn1lem10  34407  btwnconn1lem11  34408  btwnconn3  34414  brsegle  34419  seglecgr12im  34421  segleantisym  34426  outsideoftr  34440  outsideofeq  34441  outsideofeu  34442  linethru  34464  finminlem  34516  neibastop2lem  34558  isbasisrelowllem1  35535  isbasisrelowllem2  35536  mblfinlem3  35825  ftc1cnnc  35858  isbnd3  35951  heibor1lem  35976  crngm4  36170  cvlcvr1  37360  4atlem12  37633  paddasslem12  37852  paddasslem13  37853  lhpexle2lem  38030  trlord  38590  cdlemkid4  38955  dihopelvalcpre  39269  dihmeetlem1N  39311  dihglblem5apreN  39312  dihmeetlem6  39330  dih1dimatlem0  39349  dihjatcclem4  39442  prjspner1  40470  mzpcl2  40559  mzpmfp  40576  mzpcompact2lem  40580  diophin  40601  pell14qrmulcl  40692  hbtlem2  40956  iunrelexpuztr  41334  stoweidlem61  43609  fourierdlem92  43746  euoreqb  44612  prproropf1olem3  44968  prproropf1olem4  44969  fpprwpprb  45203  snlindsntor  45823  elfzolborelfzop1  45871  nn0sumshdiglemB  45977