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  7295  fliftfun  7320  fprresex  8328  domunfican  9313  finsschain  9348  suppeqfsuppbi  9371  fsuppunbi  9381  wemapsolem  9544  wemapso  9545  wemapso2lem  9546  cantnf  9694  enfin2i  10399  ttukeylem7  10593  fpwwe2lem2  10717  fpwwe2lem8  10723  fpwwe2lem11  10726  fpwwelem  10730  distrlem4pr  11111  mulcmpblnr  11156  prsrlem1  11157  addsrmo  11158  mulsrmo  11159  divdivdiv  12018  divsubdiv  12033  lediv12a  12210  xmullem  13394  xlemul1a  13418  seqcaopr  14182  leexp2r  14317  hashf1lem1  14600  hashf1lem2  14601  fi1uzind  14652  brfi1indALT  14655  wrd2ind  14872  swrdccat  14884  cshweqrep  14972  rtrclreclem4  15214  summolem2  15882  summo  15883  prodmolem2  16102  prodmo  16103  bezoutlem3  16714  bezoutlem4  16715  qredeu  16833  pcadd  17067  vdwlem9  17167  vdwlem10  17168  ramub1lem2  17205  ramub1  17206  cofucl  18063  setcmon  18262  poslubmo  18583  posglbmo  18584  grprcan  19184  isnsg3  19370  ghmpreima  19452  gaorber  19522  psgneu  19720  odcau  19818  lsmsubm  19867  lsmmod  19889  efgsfo  19953  ablfaclem3  20303  rngpropd  20396  ringpropd  20519  islmodd  21141  lmodprop2d  21199  lss1d  21238  lindff1  22126  islindf4  22144  assamulgscmlem2  22208  mplcoe1  22346  mplcoe5  22349  evlslem1  22391  mdetunilem7  22933  mdetunilem8  22934  mdetunilem9  22935  mdetuni0  22936  mdetmul  22938  ppttop  23325  epttop  23327  cnhaus  23672  isreg2  23695  cncmp  23710  1stcfb  23763  2ndcomap  23777  cldllycmp  23814  txcls  23923  ptclsg  23934  ptcnp  23941  txdis1cn  23954  txlly  23955  txnlly  23956  pthaus  23957  txhaus  23966  txkgen  23971  xkohaus  23972  xkococnlem  23978  xkococn  23979  fgabs  24198  rnelfm  24272  hausflimi  24299  hausflim  24300  alexsubALTlem2  24367  alexsubALTlem4  24369  alexsubALT  24370  tgpconncomp  24432  qustgplem  24440  metequiv2  24829  met2ndci  24841  nrmmetd  24893  nlmvscnlem1  25005  reconn  25148  xrge0tsms  25154  ipcnlem1  25566  minveclem3  25750  pmltpc  25771  ovolicc2lem5  25842  ovolicc2  25843  uniioombllem6  25909  dyadmbllem  25920  vitalilem3  25931  mbfmullem  26046  itg2split  26070  itg2mono  26074  bddiblnc  26162  dvlip2  26315  lhop1  26334  dvcnvrelem1  26337  ftc1lem6  26361  itgsubst  26369  dgrco  26594  plyexmo  26636  ulmdvlem3  26729  abelthlem2  26759  abelthlem8  26766  mpodvdsmulf1o  27521  dvdsmulf1o  27523  chpchtsum  27546  dchrptlem2  27592  2sqlem5  27749  2sqlem9  27754  2sqb  27759  pntrlog2bnd  27911  pntibndlem3  27919  pntlemp  27937  pnt3  27939  noresle  28054  nosupprefixmo  28057  noinfprefixmo  28058  addsprop  28362  mulsproplem9  28510  mulsasslem3  28551  oncutlt  28650  expadds  28821  bdayfinbndlem1  28853  readdscl  28885  tgjustf  28935  hlcgreu  29084  mirreu3  29126  cgraswap  29327  cgracom  29329  cgratr  29330  flatcgra  29332  acopyeu  29342  brprlng  29416  axsegcon  29505  ax5seglem9  29515  axeuclid  29541  axcontlem12  29553  clwwlkf1  30640  n4cyclfrgr  30892  frgrnbnb  30894  ablo4  31152  smcnlem  31299  pjhthmo  31904  pjpjpre  32021  3oalem2  32265  lnconi  32635  atom1d  32955  resf1o  33364  mgcoval  33589  xrge0tsmsd  33676  erlval  33861  ballotlemfc0  35167  ballotlemfcc  35168  pconnconn  36038  cvmfolem  36086  cvmliftmo  36091  cvmliftlem7  36098  cvmlift2lem10  36119  cvmlift3lem8  36133  lineext  36883  linecgr  36888  btwnconn1lem10  36903  btwnconn1lem11  36904  btwnconn3  36910  brsegle  36915  seglecgr12im  36917  segleantisym  36922  outsideoftr  36936  outsideofeq  36937  outsideofeu  36938  linethru  36960  nadddilem1  37011  finminlem  37148  neibastop2lem  37190  weiunpo  37295  isbasisrelowllem1  38321  isbasisrelowllem2  38322  mblfinlem3  38620  ftc1cnnc  38653  isbnd3  38761  heibor1lem  38786  crngm4  38980  cvlcvr1  40439  4atlem12  40712  paddasslem12  40931  paddasslem13  40932  lhpexle2lem  41109  trlord  41669  cdlemkid4  42034  dihopelvalcpre  42348  dihmeetlem1N  42390  dihglblem5apreN  42391  dihmeetlem6  42409  dih1dimatlem0  42428  dihjatcclem4  42521  unitscyglem4  43291  mzpcl2  43784  mzpmfp  43801  mzpcompact2lem  43805  diophin  43826  pell14qrmulcl  43913  hbtlem2  44169  iunrelexpuztr  44762  stoweidlem61  47114  fourierdlem92  47251  euoreqb  48222  prproropf1olem3  48630  prproropf1olem4  48631  fpprwpprb  48881  cycldlenngric  49069  grimgrtri  49090  snlindsntor  49626  elfzolborelfzop1  49674  nn0sumshdiglemB  49775  2arwcat  50751