Theorem simprlr 779

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 728	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  7228  fliftfun  7253  fprresex  8250  domunfican  9230  finsschain  9268  suppeqfsuppbi  9288  fsuppunbi  9298  wemapsolem  9461  wemapso  9462  wemapso2lem  9463  cantnf  9608  enfin2i  10234  ttukeylem7  10428  fpwwe2lem2  10545  fpwwe2lem8  10551  fpwwe2lem11  10554  fpwwelem  10558  distrlem4pr  10939  mulcmpblnr  10984  prsrlem1  10985  addsrmo  10986  mulsrmo  10987  divdivdiv  11843  divsubdiv  11858  lediv12a  12036  xmullem  13184  xlemul1a  13208  seqcaopr  13964  leexp2r  14099  hashf1lem1  14380  hashf1lem2  14381  fi1uzind  14432  brfi1indALT  14435  wrd2ind  14647  swrdccat  14659  cshweqrep  14745  rtrclreclem4  14986  summolem2  15641  summo  15642  prodmolem2  15860  prodmo  15861  bezoutlem3  16470  bezoutlem4  16471  qredeu  16587  pcadd  16819  vdwlem9  16919  vdwlem10  16920  ramub1lem2  16957  ramub1  16958  cofucl  17813  setcmon  18012  poslubmo  18333  posglbmo  18334  grprcan  18870  isnsg3  19057  ghmpreima  19135  gaorber  19205  psgneu  19403  odcau  19501  lsmsubm  19550  lsmmod  19572  efgsfo  19636  ablfaclem3  19986  rngpropd  20077  ringpropd  20191  islmodd  20787  lmodprop2d  20845  lss1d  20884  lindff1  21745  islindf4  21763  assamulgscmlem2  21825  mplcoe1  21960  mplcoe5  21963  evlslem1  22005  mdetunilem7  22521  mdetunilem8  22522  mdetunilem9  22523  mdetuni0  22524  mdetmul  22526  ppttop  22910  epttop  22912  cnhaus  23257  isreg2  23280  cncmp  23295  1stcfb  23348  2ndcomap  23361  cldllycmp  23398  txcls  23507  ptclsg  23518  ptcnp  23525  txdis1cn  23538  txlly  23539  txnlly  23540  pthaus  23541  txhaus  23550  txkgen  23555  xkohaus  23556  xkococnlem  23562  xkococn  23563  fgabs  23782  rnelfm  23856  hausflimi  23883  hausflim  23884  alexsubALTlem2  23951  alexsubALTlem4  23953  alexsubALT  23954  tgpconncomp  24016  qustgplem  24024  metequiv2  24414  met2ndci  24426  nrmmetd  24478  nlmvscnlem1  24590  reconn  24733  xrge0tsms  24739  ipcnlem1  25161  minveclem3  25345  pmltpc  25367  ovolicc2lem5  25438  ovolicc2  25439  uniioombllem6  25505  dyadmbllem  25516  vitalilem3  25527  mbfmullem  25642  itg2split  25666  itg2mono  25670  bddiblnc  25759  dvlip2  25916  lhop1  25935  dvcnvrelem1  25938  ftc1lem6  25964  itgsubst  25972  dgrco  26197  plyexmo  26237  ulmdvlem3  26327  abelthlem2  26358  abelthlem8  26365  mpodvdsmulf1o  27120  dvdsmulf1o  27122  chpchtsum  27146  dchrptlem2  27192  2sqlem5  27349  2sqlem9  27354  2sqb  27359  pntrlog2bnd  27511  pntibndlem3  27519  pntlemp  27537  pnt3  27539  noresle  27625  nosupprefixmo  27628  noinfprefixmo  27629  addsprop  27906  mulsproplem9  28050  mulsasslem3  28091  onscutlt  28188  expadds  28345  readdscl  28386  tgjustf  28436  hlcgreu  28581  mirreu3  28617  cgraswap  28783  cgracom  28785  cgratr  28786  flatcgra  28787  acopyeu  28797  axsegcon  28890  ax5seglem9  28900  axeuclid  28926  axcontlem12  28938  clwwlkf1  30011  n4cyclfrgr  30253  frgrnbnb  30255  ablo4  30512  smcnlem  30659  pjhthmo  31264  pjpjpre  31381  3oalem2  31625  lnconi  31995  atom1d  32315  resf1o  32686  mgcoval  32941  xrge0tsmsd  33028  erlval  33208  ballotlemfc0  34460  ballotlemfcc  34461  pconnconn  35203  cvmfolem  35251  cvmliftmo  35256  cvmliftlem7  35263  cvmlift2lem10  35284  cvmlift3lem8  35298  lineext  36049  linecgr  36054  btwnconn1lem10  36069  btwnconn1lem11  36070  btwnconn3  36076  brsegle  36081  seglecgr12im  36083  segleantisym  36088  outsideoftr  36102  outsideofeq  36103  outsideofeu  36104  linethru  36126  finminlem  36291  neibastop2lem  36333  weiunpo  36438  isbasisrelowllem1  37328  isbasisrelowllem2  37329  mblfinlem3  37638  ftc1cnnc  37671  isbnd3  37763  heibor1lem  37788  crngm4  37982  cvlcvr1  39317  4atlem12  39591  paddasslem12  39810  paddasslem13  39811  lhpexle2lem  39988  trlord  40548  cdlemkid4  40913  dihopelvalcpre  41227  dihmeetlem1N  41269  dihglblem5apreN  41270  dihmeetlem6  41288  dih1dimatlem0  41307  dihjatcclem4  41400  unitscyglem4  42171  prjspner1  42599  mzpcl2  42703  mzpmfp  42720  mzpcompact2lem  42724  diophin  42745  pell14qrmulcl  42836  hbtlem2  43097  iunrelexpuztr  43692  stoweidlem61  46043  fourierdlem92  46180  euoreqb  47094  prproropf1olem3  47490  prproropf1olem4  47491  fpprwpprb  47725  cycldlenngric  47912  grimgrtri  47932  snlindsntor  48444  elfzolborelfzop1  48492  nn0sumshdiglemB  48593  2arwcat  49573