Theorem simprlr 792

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fcof1  7318  fliftfun  7343  fprresex  8356  domunfican  9341  finsschain  9376  suppeqfsuppbi  9398  fsuppunbi  9408  wemapsolem  9571  wemapso  9572  wemapso2lem  9573  cantnf  9721  enfin2i  10426  ttukeylem7  10620  fpwwe2lem2  10744  fpwwe2lem8  10750  fpwwe2lem11  10753  fpwwelem  10757  distrlem4pr  11138  mulcmpblnr  11183  prsrlem1  11184  addsrmo  11185  mulsrmo  11186  divdivdiv  12045  divsubdiv  12060  lediv12a  12237  xmullem  13421  xlemul1a  13445  seqcaopr  14209  leexp2r  14344  hashf1lem1  14627  hashf1lem2  14628  fi1uzind  14679  brfi1indALT  14682  wrd2ind  14900  swrdccat  14912  cshweqrep  15000  rtrclreclem4  15243  summolem2  15911  summo  15912  prodmolem2  16131  prodmo  16132  bezoutlem3  16743  bezoutlem4  16744  qredeu  16862  pcadd  17096  vdwlem9  17196  vdwlem10  17197  ramub1lem2  17234  ramub1  17235  cofucl  18092  setcmon  18291  poslubmo  18612  posglbmo  18613  grprcan  19213  isnsg3  19399  ghmpreima  19481  gaorber  19552  psgneu  19750  odcau  19848  lsmsubm  19897  lsmmod  19919  efgsfo  19983  ablfaclem3  20333  rngpropd  20426  ringpropd  20549  islmodd  21171  lmodprop2d  21229  lss1d  21268  lindff1  22156  islindf4  22174  assamulgscmlem2  22238  mplcoe1  22376  mplcoe5  22379  evlslem1  22421  mdetunilem7  22963  mdetunilem8  22964  mdetunilem9  22965  mdetuni0  22966  mdetmul  22968  ppttop  23355  epttop  23357  cnhaus  23702  isreg2  23725  cncmp  23740  1stcfb  23793  2ndcomap  23807  cldllycmp  23844  txcls  23953  ptclsg  23964  ptcnp  23971  txdis1cn  23984  txlly  23985  txnlly  23986  pthaus  23987  txhaus  23996  txkgen  24001  xkohaus  24002  xkococnlem  24008  xkococn  24009  fgabs  24228  rnelfm  24302  hausflimi  24329  hausflim  24330  alexsubALTlem2  24397  alexsubALTlem4  24399  alexsubALT  24400  tgpconncomp  24462  qustgplem  24470  metequiv2  24859  met2ndci  24871  nrmmetd  24923  nlmvscnlem1  25035  reconn  25178  xrge0tsms  25184  ipcnlem1  25596  minveclem3  25780  pmltpc  25801  ovolicc2lem5  25872  ovolicc2  25873  uniioombllem6  25939  dyadmbllem  25950  vitalilem3  25961  mbfmullem  26076  itg2split  26100  itg2mono  26104  bddiblnc  26192  dvlip2  26345  lhop1  26364  dvcnvrelem1  26367  ftc1lem6  26391  itgsubst  26399  dgrco  26624  plyexmo  26666  ulmdvlem3  26759  abelthlem2  26789  abelthlem8  26796  mpodvdsmulf1o  27551  dvdsmulf1o  27553  chpchtsum  27576  dchrptlem2  27622  2sqlem5  27779  2sqlem9  27784  2sqb  27789  pntrlog2bnd  27941  pntibndlem3  27949  pntlemp  27967  pnt3  27969  noresle  28084  nosupprefixmo  28087  noinfprefixmo  28088  addsprop  28392  mulsproplem9  28540  mulsasslem3  28581  oncutlt  28680  expadds  28851  bdayfinbndlem1  28883  readdscl  28915  tgjustf  28965  hlcgreu  29114  mirreu3  29156  cgraswap  29357  cgracom  29359  cgratr  29360  flatcgra  29362  acopyeu  29372  brprlng  29446  axsegcon  29535  ax5seglem9  29545  axeuclid  29571  axcontlem12  29583  clwwlkf1  30670  n4cyclfrgr  30922  frgrnbnb  30924  ablo4  31182  smcnlem  31329  pjhthmo  31934  pjpjpre  32051  3oalem2  32295  lnconi  32665  atom1d  32985  resf1o  33392  mgcoval  33617  xrge0tsmsd  33704  erlval  33889  ballotlemfc0  35195  ballotlemfcc  35196  pconnconn  36163  cvmfolem  36211  cvmliftmo  36216  cvmliftlem7  36223  cvmlift2lem10  36244  cvmlift3lem8  36258  lineext  37019  linecgr  37024  btwnconn1lem10  37039  btwnconn1lem11  37040  btwnconn3  37046  brsegle  37051  seglecgr12im  37053  segleantisym  37058  outsideoftr  37072  outsideofeq  37073  outsideofeu  37074  linethru  37096  nadddilem1  37147  finminlem  37284  neibastop2lem  37326  weiunpo  37431  isbasisrelowllem1  38470  isbasisrelowllem2  38471  mblfinlem3  38769  ftc1cnnc  38802  isbnd3  38910  heibor1lem  38935  crngm4  39129  cvlcvr1  40588  4atlem12  40861  paddasslem12  41080  paddasslem13  41081  lhpexle2lem  41258  trlord  41818  cdlemkid4  42183  dihopelvalcpre  42497  dihmeetlem1N  42539  dihglblem5apreN  42540  dihmeetlem6  42558  dih1dimatlem0  42577  dihjatcclem4  42670  unitscyglem4  43440  mzpcl2  43934  mzpmfp  43951  mzpcompact2lem  43955  diophin  43976  pell14qrmulcl  44063  hbtlem2  44318  iunrelexpuztr  44911  stoweidlem61  47276  fourierdlem92  47413  euoreqb  48385  prproropf1olem3  48792  prproropf1olem4  48793  fpprwpprb  49043  cycldlenngric  49231  grimgrtri  49252  snlindsntor  49788  elfzolborelfzop1  49836  nn0sumshdiglemB  49937  2arwcat  50943