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 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

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

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 401

This theorem is used by:  fcof1  7285  fliftfun  7310  fprresex  8305  domunfican  9279  finsschain  9314  suppeqfsuppbi  9337  fsuppunbi  9347  wemapsolem  9510  wemapso  9511  wemapso2lem  9512  cantnf  9660  enfin2i  10311  ttukeylem7  10505  fpwwe2lem2  10623  fpwwe2lem8  10629  fpwwe2lem11  10632  fpwwelem  10636  distrlem4pr  11017  mulcmpblnr  11062  prsrlem1  11063  addsrmo  11064  mulsrmo  11065  divdivdiv  11922  divsubdiv  11937  lediv12a  12114  xmullem  13296  xlemul1a  13320  seqcaopr  14082  leexp2r  14217  hashf1lem1  14499  hashf1lem2  14500  fi1uzind  14551  brfi1indALT  14554  wrd2ind  14767  swrdccat  14779  cshweqrep  14865  rtrclreclem4  15105  summolem2  15774  summo  15775  prodmolem2  15996  prodmo  15997  bezoutlem3  16605  bezoutlem4  16606  qredeu  16722  pcadd  16955  vdwlem9  17055  vdwlem10  17056  ramub1lem2  17093  ramub1  17094  cofucl  17951  setcmon  18150  poslubmo  18471  posglbmo  18472  grprcan  19046  isnsg3  19232  ghmpreima  19314  gaorber  19384  psgneu  19582  odcau  19680  lsmsubm  19729  lsmmod  19751  efgsfo  19815  ablfaclem3  20165  rngpropd  20258  ringpropd  20378  islmodd  20998  lmodprop2d  21056  lss1d  21095  lindff1  21981  islindf4  21999  assamulgscmlem2  22061  mplcoe1  22199  mplcoe5  22202  evlslem1  22244  mdetunilem7  22786  mdetunilem8  22787  mdetunilem9  22788  mdetuni0  22789  mdetmul  22791  ppttop  23175  epttop  23177  cnhaus  23522  isreg2  23545  cncmp  23560  1stcfb  23613  2ndcomap  23626  cldllycmp  23663  txcls  23772  ptclsg  23783  ptcnp  23790  txdis1cn  23803  txlly  23804  txnlly  23805  pthaus  23806  txhaus  23815  txkgen  23820  xkohaus  23821  xkococnlem  23827  xkococn  23828  fgabs  24047  rnelfm  24121  hausflimi  24148  hausflim  24149  alexsubALTlem2  24216  alexsubALTlem4  24218  alexsubALT  24219  tgpconncomp  24281  qustgplem  24289  metequiv2  24678  met2ndci  24690  nrmmetd  24742  nlmvscnlem1  24854  reconn  24997  xrge0tsms  25003  ipcnlem1  25415  minveclem3  25599  pmltpc  25620  ovolicc2lem5  25691  ovolicc2  25692  uniioombllem6  25758  dyadmbllem  25769  vitalilem3  25780  mbfmullem  25895  itg2split  25919  itg2mono  25923  bddiblnc  26012  dvlip2  26165  lhop1  26184  dvcnvrelem1  26187  ftc1lem6  26211  itgsubst  26219  dgrco  26443  plyexmo  26485  ulmdvlem3  26576  abelthlem2  26606  abelthlem8  26613  mpodvdsmulf1o  27369  dvdsmulf1o  27371  chpchtsum  27394  dchrptlem2  27440  2sqlem5  27597  2sqlem9  27602  2sqb  27607  pntrlog2bnd  27759  pntibndlem3  27767  pntlemp  27785  pnt3  27787  noresle  27872  nosupprefixmo  27875  noinfprefixmo  27876  addsprop  28180  mulsproplem9  28328  mulsasslem3  28369  oncutlt  28468  expadds  28639  bdayfinbndlem1  28671  readdscl  28703  tgjustf  28753  hlcgreu  28901  mirreu3  28942  cgraswap  29142  cgracom  29144  cgratr  29145  flatcgra  29146  acopyeu  29156  brprlng  29199  axsegcon  29288  ax5seglem9  29298  axeuclid  29324  axcontlem12  29336  clwwlkf1  30411  n4cyclfrgr  30653  frgrnbnb  30655  ablo4  30913  smcnlem  31060  pjhthmo  31665  pjpjpre  31782  3oalem2  32026  lnconi  32396  atom1d  32716  resf1o  33086  mgcoval  33315  xrge0tsmsd  33402  erlval  33587  ballotlemfc0  34892  ballotlemfcc  34893  pconnconn  35731  cvmfolem  35779  cvmliftmo  35784  cvmliftlem7  35791  cvmlift2lem10  35812  cvmlift3lem8  35826  lineext  36576  linecgr  36581  btwnconn1lem10  36596  btwnconn1lem11  36597  btwnconn3  36603  brsegle  36608  seglecgr12im  36610  segleantisym  36615  outsideoftr  36629  outsideofeq  36630  outsideofeu  36631  linethru  36653  nadddilem1  36720  finminlem  36857  neibastop2lem  36899  weiunpo  37004  isbasisrelowllem1  38029  isbasisrelowllem2  38030  mblfinlem3  38338  ftc1cnnc  38371  isbnd3  38463  heibor1lem  38488  crngm4  38682  cvlcvr1  40141  4atlem12  40414  paddasslem12  40633  paddasslem13  40634  lhpexle2lem  40811  trlord  41371  cdlemkid4  41736  dihopelvalcpre  42050  dihmeetlem1N  42092  dihglblem5apreN  42093  dihmeetlem6  42111  dih1dimatlem0  42130  dihjatcclem4  42223  unitscyglem4  42993  prjspner1  43386  mzpcl2  43489  mzpmfp  43506  mzpcompact2lem  43510  diophin  43531  pell14qrmulcl  43618  hbtlem2  43879  iunrelexpuztr  44473  stoweidlem61  46803  fourierdlem92  46940  euoreqb  47874  prproropf1olem3  48282  prproropf1olem4  48283  fpprwpprb  48533  cycldlenngric  48721  grimgrtri  48742  snlindsntor  49279  elfzolborelfzop1  49327  nn0sumshdiglemB  49428  2arwcat  50406