Theorem simprlr 791

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fcof1  7285  fliftfun  7310  fprresex  8306  domunfican  9280  finsschain  9315  suppeqfsuppbi  9338  fsuppunbi  9348  wemapsolem  9511  wemapso  9512  wemapso2lem  9513  cantnf  9661  enfin2i  10304  ttukeylem7  10498  fpwwe2lem2  10616  fpwwe2lem8  10622  fpwwe2lem11  10625  fpwwelem  10629  distrlem4pr  11010  mulcmpblnr  11055  prsrlem1  11056  addsrmo  11057  mulsrmo  11058  divdivdiv  11915  divsubdiv  11930  lediv12a  12107  xmullem  13289  xlemul1a  13313  seqcaopr  14074  leexp2r  14209  hashf1lem1  14491  hashf1lem2  14492  fi1uzind  14543  brfi1indALT  14546  wrd2ind  14759  swrdccat  14771  cshweqrep  14857  rtrclreclem4  15097  summolem2  15766  summo  15767  prodmolem2  15988  prodmo  15989  bezoutlem3  16598  bezoutlem4  16599  qredeu  16715  pcadd  16948  vdwlem9  17048  vdwlem10  17049  ramub1lem2  17086  ramub1  17087  cofucl  17944  setcmon  18143  poslubmo  18464  posglbmo  18465  grprcan  19039  isnsg3  19225  ghmpreima  19307  gaorber  19377  psgneu  19575  odcau  19673  lsmsubm  19722  lsmmod  19744  efgsfo  19808  ablfaclem3  20158  rngpropd  20251  ringpropd  20370  islmodd  20966  lmodprop2d  21024  lss1d  21063  lindff1  21949  islindf4  21967  assamulgscmlem2  22029  mplcoe1  22167  mplcoe5  22170  evlslem1  22212  mdetunilem7  22754  mdetunilem8  22755  mdetunilem9  22756  mdetuni0  22757  mdetmul  22759  ppttop  23143  epttop  23145  cnhaus  23490  isreg2  23513  cncmp  23528  1stcfb  23581  2ndcomap  23594  cldllycmp  23631  txcls  23740  ptclsg  23751  ptcnp  23758  txdis1cn  23771  txlly  23772  txnlly  23773  pthaus  23774  txhaus  23783  txkgen  23788  xkohaus  23789  xkococnlem  23795  xkococn  23796  fgabs  24015  rnelfm  24089  hausflimi  24116  hausflim  24117  alexsubALTlem2  24184  alexsubALTlem4  24186  alexsubALT  24187  tgpconncomp  24249  qustgplem  24257  metequiv2  24646  met2ndci  24658  nrmmetd  24710  nlmvscnlem1  24822  reconn  24965  xrge0tsms  24971  ipcnlem1  25383  minveclem3  25567  pmltpc  25588  ovolicc2lem5  25659  ovolicc2  25660  uniioombllem6  25726  dyadmbllem  25737  vitalilem3  25748  mbfmullem  25863  itg2split  25887  itg2mono  25891  bddiblnc  25980  dvlip2  26133  lhop1  26152  dvcnvrelem1  26155  ftc1lem6  26179  itgsubst  26187  dgrco  26411  plyexmo  26453  ulmdvlem3  26541  abelthlem2  26571  abelthlem8  26578  mpodvdsmulf1o  27334  dvdsmulf1o  27336  chpchtsum  27359  dchrptlem2  27405  2sqlem5  27562  2sqlem9  27567  2sqb  27572  pntrlog2bnd  27724  pntibndlem3  27732  pntlemp  27750  pnt3  27752  noresle  27837  nosupprefixmo  27840  noinfprefixmo  27841  addsprop  28145  mulsproplem9  28293  mulsasslem3  28334  oncutlt  28433  expadds  28604  bdayfinbndlem1  28636  readdscl  28668  tgjustf  28718  hlcgreu  28866  mirreu3  28907  cgraswap  29104  cgracom  29106  cgratr  29107  flatcgra  29108  acopyeu  29118  brprlng  29161  axsegcon  29243  ax5seglem9  29253  axeuclid  29279  axcontlem12  29291  clwwlkf1  30366  n4cyclfrgr  30608  frgrnbnb  30610  ablo4  30868  smcnlem  31015  pjhthmo  31620  pjpjpre  31737  3oalem2  31981  lnconi  32351  atom1d  32671  resf1o  33041  mgcoval  33272  xrge0tsmsd  33359  erlval  33544  ballotlemfc0  34849  ballotlemfcc  34850  pconnconn  35677  cvmfolem  35725  cvmliftmo  35730  cvmliftlem7  35737  cvmlift2lem10  35758  cvmlift3lem8  35772  lineext  36522  linecgr  36527  btwnconn1lem10  36542  btwnconn1lem11  36543  btwnconn3  36549  brsegle  36554  seglecgr12im  36556  segleantisym  36561  outsideoftr  36575  outsideofeq  36576  outsideofeu  36577  linethru  36599  finminlem  36773  neibastop2lem  36815  weiunpo  36920  isbasisrelowllem1  37945  isbasisrelowllem2  37946  mblfinlem3  38254  ftc1cnnc  38287  isbnd3  38379  heibor1lem  38404  crngm4  38598  cvlcvr1  40059  4atlem12  40332  paddasslem12  40551  paddasslem13  40552  lhpexle2lem  40729  trlord  41289  cdlemkid4  41654  dihopelvalcpre  41968  dihmeetlem1N  42010  dihglblem5apreN  42011  dihmeetlem6  42029  dih1dimatlem0  42048  dihjatcclem4  42141  unitscyglem4  42911  prjspner1  43306  mzpcl2  43409  mzpmfp  43426  mzpcompact2lem  43430  diophin  43451  pell14qrmulcl  43538  hbtlem2  43799  iunrelexpuztr  44393  stoweidlem61  46723  fourierdlem92  46860  euoreqb  47791  prproropf1olem3  48199  prproropf1olem4  48200  fpprwpprb  48450  cycldlenngric  48638  grimgrtri  48659  snlindsntor  49196  elfzolborelfzop1  49244  nn0sumshdiglemB  49345  2arwcat  50323