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  7236  fliftfun  7261  fprresex  8255  domunfican  9227  finsschain  9264  suppeqfsuppbi  9287  fsuppunbi  9297  wemapsolem  9460  wemapso  9461  wemapso2lem  9462  cantnf  9607  enfin2i  10236  ttukeylem7  10430  fpwwe2lem2  10548  fpwwe2lem8  10554  fpwwe2lem11  10557  fpwwelem  10561  distrlem4pr  10942  mulcmpblnr  10987  prsrlem1  10988  addsrmo  10989  mulsrmo  10990  divdivdiv  11847  divsubdiv  11862  lediv12a  12040  xmullem  13184  xlemul1a  13208  seqcaopr  13967  leexp2r  14102  hashf1lem1  14383  hashf1lem2  14384  fi1uzind  14435  brfi1indALT  14438  wrd2ind  14651  swrdccat  14663  cshweqrep  14749  rtrclreclem4  14989  summolem2  15644  summo  15645  prodmolem2  15863  prodmo  15864  bezoutlem3  16473  bezoutlem4  16474  qredeu  16590  pcadd  16822  vdwlem9  16922  vdwlem10  16923  ramub1lem2  16960  ramub1  16961  cofucl  17817  setcmon  18016  poslubmo  18337  posglbmo  18338  grprcan  18908  isnsg3  19094  ghmpreima  19172  gaorber  19242  psgneu  19440  odcau  19538  lsmsubm  19587  lsmmod  19609  efgsfo  19673  ablfaclem3  20023  rngpropd  20114  ringpropd  20228  islmodd  20822  lmodprop2d  20880  lss1d  20919  lindff1  21780  islindf4  21798  assamulgscmlem2  21861  mplcoe1  21997  mplcoe5  22000  evlslem1  22042  mdetunilem7  22567  mdetunilem8  22568  mdetunilem9  22569  mdetuni0  22570  mdetmul  22572  ppttop  22956  epttop  22958  cnhaus  23303  isreg2  23326  cncmp  23341  1stcfb  23394  2ndcomap  23407  cldllycmp  23444  txcls  23553  ptclsg  23564  ptcnp  23571  txdis1cn  23584  txlly  23585  txnlly  23586  pthaus  23587  txhaus  23596  txkgen  23601  xkohaus  23602  xkococnlem  23608  xkococn  23609  fgabs  23828  rnelfm  23902  hausflimi  23929  hausflim  23930  alexsubALTlem2  23997  alexsubALTlem4  23999  alexsubALT  24000  tgpconncomp  24062  qustgplem  24070  metequiv2  24459  met2ndci  24471  nrmmetd  24523  nlmvscnlem1  24635  reconn  24778  xrge0tsms  24784  ipcnlem1  25206  minveclem3  25390  pmltpc  25412  ovolicc2lem5  25483  ovolicc2  25484  uniioombllem6  25550  dyadmbllem  25561  vitalilem3  25572  mbfmullem  25687  itg2split  25711  itg2mono  25715  bddiblnc  25804  dvlip2  25961  lhop1  25980  dvcnvrelem1  25983  ftc1lem6  26009  itgsubst  26017  dgrco  26242  plyexmo  26282  ulmdvlem3  26372  abelthlem2  26403  abelthlem8  26410  mpodvdsmulf1o  27165  dvdsmulf1o  27167  chpchtsum  27191  dchrptlem2  27237  2sqlem5  27394  2sqlem9  27399  2sqb  27404  pntrlog2bnd  27556  pntibndlem3  27564  pntlemp  27582  pnt3  27584  noresle  27670  nosupprefixmo  27673  noinfprefixmo  27674  addsprop  27977  mulsproplem9  28125  mulsasslem3  28166  oncutlt  28265  expadds  28436  bdayfinbndlem1  28468  readdscl  28500  tgjustf  28550  hlcgreu  28695  mirreu3  28731  cgraswap  28897  cgracom  28899  cgratr  28900  flatcgra  28901  acopyeu  28911  axsegcon  29005  ax5seglem9  29015  axeuclid  29041  axcontlem12  29053  clwwlkf1  30129  n4cyclfrgr  30371  frgrnbnb  30373  ablo4  30630  smcnlem  30777  pjhthmo  31382  pjpjpre  31499  3oalem2  31743  lnconi  32113  atom1d  32433  resf1o  32812  mgcoval  33071  xrge0tsmsd  33159  erlval  33344  ballotlemfc0  34663  ballotlemfcc  34664  pconnconn  35438  cvmfolem  35486  cvmliftmo  35491  cvmliftlem7  35498  cvmlift2lem10  35519  cvmlift3lem8  35533  lineext  36283  linecgr  36288  btwnconn1lem10  36303  btwnconn1lem11  36304  btwnconn3  36310  brsegle  36315  seglecgr12im  36317  segleantisym  36322  outsideoftr  36336  outsideofeq  36337  outsideofeu  36338  linethru  36360  finminlem  36525  neibastop2lem  36567  weiunpo  36672  isbasisrelowllem1  37573  isbasisrelowllem2  37574  mblfinlem3  37873  ftc1cnnc  37906  isbnd3  37998  heibor1lem  38023  crngm4  38217  cvlcvr1  39678  4atlem12  39951  paddasslem12  40170  paddasslem13  40171  lhpexle2lem  40348  trlord  40908  cdlemkid4  41273  dihopelvalcpre  41587  dihmeetlem1N  41629  dihglblem5apreN  41630  dihmeetlem6  41648  dih1dimatlem0  41667  dihjatcclem4  41760  unitscyglem4  42531  prjspner1  42947  mzpcl2  43050  mzpmfp  43067  mzpcompact2lem  43071  diophin  43092  pell14qrmulcl  43183  hbtlem2  43444  iunrelexpuztr  44038  stoweidlem61  46382  fourierdlem92  46519  euoreqb  47432  prproropf1olem3  47828  prproropf1olem4  47829  fpprwpprb  48063  cycldlenngric  48251  grimgrtri  48272  snlindsntor  48794  elfzolborelfzop1  48842  nn0sumshdiglemB  48943  2arwcat  49922