Theorem simprlr 780

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 729	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  7231  fliftfun  7256  fprresex  8249  domunfican  9221  finsschain  9258  suppeqfsuppbi  9281  fsuppunbi  9291  wemapsolem  9454  wemapso  9455  wemapso2lem  9456  cantnf  9603  enfin2i  10232  ttukeylem7  10426  fpwwe2lem2  10544  fpwwe2lem8  10550  fpwwe2lem11  10553  fpwwelem  10557  distrlem4pr  10938  mulcmpblnr  10983  prsrlem1  10984  addsrmo  10985  mulsrmo  10986  divdivdiv  11845  divsubdiv  11860  lediv12a  12038  xmullem  13205  xlemul1a  13229  seqcaopr  13990  leexp2r  14125  hashf1lem1  14406  hashf1lem2  14407  fi1uzind  14458  brfi1indALT  14461  wrd2ind  14674  swrdccat  14686  cshweqrep  14772  rtrclreclem4  15012  summolem2  15667  summo  15668  prodmolem2  15889  prodmo  15890  bezoutlem3  16499  bezoutlem4  16500  qredeu  16616  pcadd  16849  vdwlem9  16949  vdwlem10  16950  ramub1lem2  16987  ramub1  16988  cofucl  17844  setcmon  18043  poslubmo  18364  posglbmo  18365  grprcan  18938  isnsg3  19124  ghmpreima  19202  gaorber  19272  psgneu  19470  odcau  19568  lsmsubm  19617  lsmmod  19639  efgsfo  19703  ablfaclem3  20053  rngpropd  20144  ringpropd  20258  islmodd  20850  lmodprop2d  20908  lss1d  20947  lindff1  21789  islindf4  21807  assamulgscmlem2  21869  mplcoe1  22004  mplcoe5  22007  evlslem1  22049  mdetunilem7  22571  mdetunilem8  22572  mdetunilem9  22573  mdetuni0  22574  mdetmul  22576  ppttop  22960  epttop  22962  cnhaus  23307  isreg2  23330  cncmp  23345  1stcfb  23398  2ndcomap  23411  cldllycmp  23448  txcls  23557  ptclsg  23568  ptcnp  23575  txdis1cn  23588  txlly  23589  txnlly  23590  pthaus  23591  txhaus  23600  txkgen  23605  xkohaus  23606  xkococnlem  23612  xkococn  23613  fgabs  23832  rnelfm  23906  hausflimi  23933  hausflim  23934  alexsubALTlem2  24001  alexsubALTlem4  24003  alexsubALT  24004  tgpconncomp  24066  qustgplem  24074  metequiv2  24463  met2ndci  24475  nrmmetd  24527  nlmvscnlem1  24639  reconn  24782  xrge0tsms  24788  ipcnlem1  25200  minveclem3  25384  pmltpc  25405  ovolicc2lem5  25476  ovolicc2  25477  uniioombllem6  25543  dyadmbllem  25554  vitalilem3  25565  mbfmullem  25680  itg2split  25704  itg2mono  25708  bddiblnc  25797  dvlip2  25950  lhop1  25969  dvcnvrelem1  25972  ftc1lem6  25996  itgsubst  26004  dgrco  26228  plyexmo  26267  ulmdvlem3  26355  abelthlem2  26385  abelthlem8  26392  mpodvdsmulf1o  27145  dvdsmulf1o  27147  chpchtsum  27170  dchrptlem2  27216  2sqlem5  27373  2sqlem9  27378  2sqb  27383  pntrlog2bnd  27535  pntibndlem3  27543  pntlemp  27561  pnt3  27563  noresle  27649  nosupprefixmo  27652  noinfprefixmo  27653  addsprop  27956  mulsproplem9  28104  mulsasslem3  28145  oncutlt  28244  expadds  28415  bdayfinbndlem1  28447  readdscl  28479  tgjustf  28529  hlcgreu  28674  mirreu3  28710  cgraswap  28876  cgracom  28878  cgratr  28879  flatcgra  28880  acopyeu  28890  axsegcon  28984  ax5seglem9  28994  axeuclid  29020  axcontlem12  29032  clwwlkf1  30107  n4cyclfrgr  30349  frgrnbnb  30351  ablo4  30609  smcnlem  30756  pjhthmo  31361  pjpjpre  31478  3oalem2  31722  lnconi  32092  atom1d  32412  resf1o  32791  mgcoval  33034  xrge0tsmsd  33122  erlval  33307  ballotlemfc0  34625  ballotlemfcc  34626  pconnconn  35401  cvmfolem  35449  cvmliftmo  35454  cvmliftlem7  35461  cvmlift2lem10  35482  cvmlift3lem8  35496  lineext  36246  linecgr  36251  btwnconn1lem10  36266  btwnconn1lem11  36267  btwnconn3  36273  brsegle  36278  seglecgr12im  36280  segleantisym  36285  outsideoftr  36299  outsideofeq  36300  outsideofeu  36301  linethru  36323  finminlem  36488  neibastop2lem  36530  weiunpo  36635  isbasisrelowllem1  37659  isbasisrelowllem2  37660  mblfinlem3  37968  ftc1cnnc  38001  isbnd3  38093  heibor1lem  38118  crngm4  38312  cvlcvr1  39773  4atlem12  40046  paddasslem12  40265  paddasslem13  40266  lhpexle2lem  40443  trlord  41003  cdlemkid4  41368  dihopelvalcpre  41682  dihmeetlem1N  41724  dihglblem5apreN  41725  dihmeetlem6  41743  dih1dimatlem0  41762  dihjatcclem4  41855  unitscyglem4  42625  prjspner1  43047  mzpcl2  43150  mzpmfp  43167  mzpcompact2lem  43171  diophin  43192  pell14qrmulcl  43279  hbtlem2  43540  iunrelexpuztr  44134  stoweidlem61  46477  fourierdlem92  46614  euoreqb  47545  prproropf1olem3  47953  prproropf1olem4  47954  fpprwpprb  48204  cycldlenngric  48392  grimgrtri  48413  snlindsntor  48935  elfzolborelfzop1  48983  nn0sumshdiglemB  49084  2arwcat  50063