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 484	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrl 725	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 206  df-an 396

This theorem is referenced by:  fcof1  7280  fliftfun  7304  fprresex  8293  wfrlem17OLD  8323  domunfican  9319  finsschain  9358  suppeqfsuppbi  9376  fsuppunbi  9383  wemapsolem  9544  wemapso  9545  wemapso2lem  9546  cantnf  9687  enfin2i  10315  ttukeylem7  10509  fpwwe2lem2  10626  fpwwe2lem8  10632  fpwwe2lem11  10635  fpwwelem  10639  distrlem4pr  11020  mulcmpblnr  11065  prsrlem1  11066  addsrmo  11067  mulsrmo  11068  divdivdiv  11916  divsubdiv  11931  lediv12a  12108  xmullem  13246  xlemul1a  13270  seqcaopr  14007  leexp2r  14141  hashf1lem1  14418  hashf1lem1OLD  14419  hashf1lem2  14420  fi1uzind  14461  brfi1indALT  14464  wrd2ind  14676  swrdccat  14688  cshweqrep  14774  rtrclreclem4  15011  summolem2  15665  summo  15666  prodmolem2  15882  prodmo  15883  bezoutlem3  16487  bezoutlem4  16488  qredeu  16599  pcadd  16828  vdwlem9  16928  vdwlem10  16929  ramub1lem2  16966  ramub1  16967  cofucl  17844  setcmon  18046  poslubmo  18373  posglbmo  18374  grprcan  18900  isnsg3  19084  ghmpreima  19160  gaorber  19221  psgneu  19423  odcau  19521  lsmsubm  19570  lsmmod  19592  efgsfo  19656  ablfaclem3  20006  rngpropd  20076  ringpropd  20184  islmodd  20709  lmodprop2d  20767  lss1d  20807  lindff1  21710  islindf4  21728  assamulgscmlem2  21789  mplcoe1  21929  mplcoe5  21932  evlslem1  21982  mdetunilem7  22470  mdetunilem8  22471  mdetunilem9  22472  mdetuni0  22473  mdetmul  22475  ppttop  22860  epttop  22862  cnhaus  23208  isreg2  23231  cncmp  23246  1stcfb  23299  2ndcomap  23312  cldllycmp  23349  txcls  23458  ptclsg  23469  ptcnp  23476  txdis1cn  23489  txlly  23490  txnlly  23491  pthaus  23492  txhaus  23501  txkgen  23506  xkohaus  23507  xkococnlem  23513  xkococn  23514  fgabs  23733  rnelfm  23807  hausflimi  23834  hausflim  23835  alexsubALTlem2  23902  alexsubALTlem4  23904  alexsubALT  23905  tgpconncomp  23967  qustgplem  23975  metequiv2  24369  met2ndci  24381  nrmmetd  24433  nlmvscnlem1  24553  reconn  24694  xrge0tsms  24700  ipcnlem1  25123  minveclem3  25307  pmltpc  25329  ovolicc2lem5  25400  ovolicc2  25401  uniioombllem6  25467  dyadmbllem  25478  vitalilem3  25489  mbfmullem  25605  itg2split  25629  itg2mono  25633  bddiblnc  25721  dvlip2  25878  lhop1  25897  dvcnvrelem1  25900  ftc1lem6  25926  itgsubst  25934  dgrco  26160  plyexmo  26198  ulmdvlem3  26288  abelthlem2  26319  abelthlem8  26326  mpodvdsmulf1o  27076  dvdsmulf1o  27078  chpchtsum  27102  dchrptlem2  27148  2sqlem5  27305  2sqlem9  27310  2sqb  27315  pntrlog2bnd  27467  pntibndlem3  27475  pntlemp  27493  pnt3  27495  noresle  27580  nosupprefixmo  27583  noinfprefixmo  27584  addsprop  27843  mulsproplem9  27974  mulsasslem3  28015  readdscl  28177  tgjustf  28227  hlcgreu  28372  mirreu3  28408  cgraswap  28574  cgracom  28576  cgratr  28577  flatcgra  28578  acopyeu  28588  axsegcon  28688  ax5seglem9  28698  axeuclid  28724  axcontlem12  28736  clwwlkf1  29806  n4cyclfrgr  30048  frgrnbnb  30050  ablo4  30307  smcnlem  30454  pjhthmo  31059  pjpjpre  31176  3oalem2  31420  lnconi  31790  atom1d  32110  resf1o  32459  mgcoval  32658  xrge0tsmsd  32712  ballotlemfc0  34020  ballotlemfcc  34021  pconnconn  34749  cvmfolem  34797  cvmliftmo  34802  cvmliftlem7  34809  cvmlift2lem10  34830  cvmlift3lem8  34844  lineext  35580  linecgr  35585  btwnconn1lem10  35600  btwnconn1lem11  35601  btwnconn3  35607  brsegle  35612  seglecgr12im  35614  segleantisym  35619  outsideoftr  35633  outsideofeq  35634  outsideofeu  35635  linethru  35657  finminlem  35710  neibastop2lem  35752  isbasisrelowllem1  36742  isbasisrelowllem2  36743  mblfinlem3  37039  ftc1cnnc  37072  isbnd3  37164  heibor1lem  37189  crngm4  37383  cvlcvr1  38721  4atlem12  38995  paddasslem12  39214  paddasslem13  39215  lhpexle2lem  39392  trlord  39952  cdlemkid4  40317  dihopelvalcpre  40631  dihmeetlem1N  40673  dihglblem5apreN  40674  dihmeetlem6  40692  dih1dimatlem0  40711  dihjatcclem4  40804  prjspner1  41928  mzpcl2  42028  mzpmfp  42045  mzpcompact2lem  42049  diophin  42070  pell14qrmulcl  42161  hbtlem2  42426  iunrelexpuztr  43028  stoweidlem61  45331  fourierdlem92  45468  euoreqb  46371  prproropf1olem3  46727  prproropf1olem4  46728  fpprwpprb  46962  snlindsntor  47409  elfzolborelfzop1  47457  nn0sumshdiglemB  47563