Theorem simprlr 787

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  fcof1  7256  fliftfun  7281  fprresex  8275  domunfican  9251  finsschain  9288  suppeqfsuppbi  9311  fsuppunbi  9321  wemapsolem  9484  wemapso  9485  wemapso2lem  9486  cantnf  9634  enfin2i  10264  ttukeylem7  10458  fpwwe2lem2  10576  fpwwe2lem8  10582  fpwwe2lem11  10585  fpwwelem  10589  distrlem4pr  10970  mulcmpblnr  11015  prsrlem1  11016  addsrmo  11017  mulsrmo  11018  divdivdiv  11878  divsubdiv  11893  lediv12a  12071  xmullem  13253  xlemul1a  13277  seqcaopr  14038  leexp2r  14173  hashf1lem1  14454  hashf1lem2  14455  fi1uzind  14506  brfi1indALT  14509  wrd2ind  14722  swrdccat  14734  cshweqrep  14820  rtrclreclem4  15060  summolem2  15715  summo  15716  prodmolem2  15937  prodmo  15938  bezoutlem3  16547  bezoutlem4  16548  qredeu  16664  pcadd  16897  vdwlem9  16997  vdwlem10  16998  ramub1lem2  17035  ramub1  17036  cofucl  17893  setcmon  18092  poslubmo  18413  posglbmo  18414  grprcan  18987  isnsg3  19173  ghmpreima  19250  gaorber  19320  psgneu  19518  odcau  19616  lsmsubm  19665  lsmmod  19687  efgsfo  19751  ablfaclem3  20101  rngpropd  20192  ringpropd  20306  islmodd  20902  lmodprop2d  20960  lss1d  20999  lindff1  21841  islindf4  21859  assamulgscmlem2  21921  mplcoe1  22059  mplcoe5  22062  evlslem1  22104  mdetunilem7  22647  mdetunilem8  22648  mdetunilem9  22649  mdetuni0  22650  mdetmul  22652  ppttop  23036  epttop  23038  cnhaus  23383  isreg2  23406  cncmp  23421  1stcfb  23474  2ndcomap  23487  cldllycmp  23524  txcls  23633  ptclsg  23644  ptcnp  23651  txdis1cn  23664  txlly  23665  txnlly  23666  pthaus  23667  txhaus  23676  txkgen  23681  xkohaus  23682  xkococnlem  23688  xkococn  23689  fgabs  23908  rnelfm  23982  hausflimi  24009  hausflim  24010  alexsubALTlem2  24077  alexsubALTlem4  24079  alexsubALT  24080  tgpconncomp  24142  qustgplem  24150  metequiv2  24539  met2ndci  24551  nrmmetd  24603  nlmvscnlem1  24715  reconn  24858  xrge0tsms  24864  ipcnlem1  25276  minveclem3  25460  pmltpc  25481  ovolicc2lem5  25552  ovolicc2  25553  uniioombllem6  25619  dyadmbllem  25630  vitalilem3  25641  mbfmullem  25756  itg2split  25780  itg2mono  25784  bddiblnc  25873  dvlip2  26026  lhop1  26045  dvcnvrelem1  26048  ftc1lem6  26072  itgsubst  26080  dgrco  26304  plyexmo  26343  ulmdvlem3  26431  abelthlem2  26461  abelthlem8  26468  mpodvdsmulf1o  27224  dvdsmulf1o  27226  chpchtsum  27249  dchrptlem2  27295  2sqlem5  27452  2sqlem9  27457  2sqb  27462  pntrlog2bnd  27614  pntibndlem3  27622  pntlemp  27640  pnt3  27642  noresle  27727  nosupprefixmo  27730  noinfprefixmo  27731  addsprop  28035  mulsproplem9  28183  mulsasslem3  28224  oncutlt  28323  expadds  28494  bdayfinbndlem1  28526  readdscl  28558  tgjustf  28608  hlcgreu  28753  mirreu3  28789  cgraswap  28955  cgracom  28957  cgratr  28958  flatcgra  28959  acopyeu  28969  axsegcon  29063  ax5seglem9  29073  axeuclid  29099  axcontlem12  29111  clwwlkf1  30186  n4cyclfrgr  30428  frgrnbnb  30430  ablo4  30688  smcnlem  30835  pjhthmo  31440  pjpjpre  31557  3oalem2  31801  lnconi  32171  atom1d  32491  resf1o  32871  mgcoval  33114  xrge0tsmsd  33203  erlval  33388  ballotlemfc0  34734  ballotlemfcc  34735  pconnconn  35519  cvmfolem  35567  cvmliftmo  35572  cvmliftlem7  35579  cvmlift2lem10  35600  cvmlift3lem8  35614  lineext  36364  linecgr  36369  btwnconn1lem10  36384  btwnconn1lem11  36385  btwnconn3  36391  brsegle  36396  seglecgr12im  36398  segleantisym  36403  outsideoftr  36417  outsideofeq  36418  outsideofeu  36419  linethru  36441  finminlem  36616  neibastop2lem  36658  weiunpo  36763  isbasisrelowllem1  37787  isbasisrelowllem2  37788  mblfinlem3  38096  ftc1cnnc  38129  isbnd3  38221  heibor1lem  38246  crngm4  38440  cvlcvr1  39901  4atlem12  40174  paddasslem12  40393  paddasslem13  40394  lhpexle2lem  40571  trlord  41131  cdlemkid4  41496  dihopelvalcpre  41810  dihmeetlem1N  41852  dihglblem5apreN  41853  dihmeetlem6  41871  dih1dimatlem0  41890  dihjatcclem4  41983  unitscyglem4  42753  prjspner1  43146  mzpcl2  43249  mzpmfp  43266  mzpcompact2lem  43270  diophin  43291  pell14qrmulcl  43378  hbtlem2  43639  iunrelexpuztr  44233  stoweidlem61  46573  fourierdlem92  46710  euoreqb  47641  prproropf1olem3  48049  prproropf1olem4  48050  fpprwpprb  48300  cycldlenngric  48488  grimgrtri  48509  snlindsntor  49031  elfzolborelfzop1  49079  nn0sumshdiglemB  49180  2arwcat  50159