Theorem simprll 790

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprll	⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Proof of Theorem simprll

Step	Hyp	Ref	Expression
1		simpl 487	. 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  7275  mpo0  7485  fpr3g  8270  fprresex  8295  eroveu  8798  boxriin  8926  fofinf1o  9277  finsschain  9304  suppeqfsuppbi  9327  fsuppunbi  9337  marypha1lem  9381  wemapsolem  9500  wemapso  9501  wemapso2lem  9502  cantnf  9650  iunfictbso  10086  enfin2i  10293  ttukeylem7  10487  fpwwe2lem2  10605  fpwwe2lem8  10611  fpwwe2lem11  10614  fpwwelem  10618  distrlem4pr  10999  mulcmpblnr  11044  prsrlem1  11045  dedekind  11361  divdivdiv  11907  divmuleq  11911  divadddiv  11921  divsubdiv  11922  lediv12a  12099  xmullem  13281  xlemul1a  13305  seqcaopr  14066  leexp2r  14201  hashf1lem1  14482  hashf1lem2  14483  ccatsymb  14610  wrd2ind  14750  cshweqrep  14848  rtrclreclem4  15088  lo1le  15693  summolem2  15757  summo  15758  prodmolem2  15979  prodmo  15980  bezoutlem3  16589  bezoutlem4  16590  qredeu  16706  pcadd  16939  prmreclem2  16967  vdwlem9  17039  vdwlem10  17040  ramub1lem2  17077  ramub1  17078  prmgaplem7  17107  cofucl  17935  initoeu2  18063  setcmon  18134  poslubmo  18455  posglbmo  18456  rabsubmgmd  18752  issubmd  18854  grprcan  19030  isnsg3  19217  ghmpreima  19299  gaorber  19369  psgneu  19567  odcau  19665  lsmsubm  19714  lsmmod  19736  ablfaclem3  20150  rngpropd  20243  ringpropd  20362  lmodvsmmulgdi  20987  lmodprop2d  21014  lss1d  21053  lindff1  21930  islindf4  21948  assamulgscmlem2  22010  mplcoe1  22148  mplcoe5  22151  evlslem1  22193  mdetunilem7  22736  mdetunilem8  22737  mdetunilem9  22738  mdetuni0  22739  mdetmul  22741  cayhamlem3  23005  ppttop  23125  epttop  23127  cnhaus  23472  isreg2  23495  cncmp  23510  1stcfb  23563  2ndcomap  23576  1stccnp  23580  cldllycmp  23613  1stckgenlem  23671  txcls  23722  ptcnp  23740  txdis1cn  23753  txlly  23754  txnlly  23755  pthaus  23756  txhaus  23765  txkgen  23770  xkohaus  23771  xkococnlem  23777  xkococn  23778  opnfbas  23960  hausflimi  24098  hausflim  24099  hauspwpwf1  24105  alexsubALT  24169  tgpconncomp  24231  qustgplem  24239  metequiv2  24628  met2ndci  24640  nrmmetd  24692  nlmvscnlem1  24804  reconn  24947  xrge0tsms  24953  mulc1cncf  25025  ipcnlem1  25365  minveclem3  25549  pmltpc  25570  ovolicc2lem5  25641  ovolicc2  25642  uniioombllem6  25708  dyadmbllem  25719  vitalilem3  25730  mbfmullem  25845  itg2split  25869  itg2mono  25873  bddiblnc  25962  dvlip2  26115  lhop1  26134  dvcnvrelem1  26137  dvfsumrlim  26151  ftc1lem6  26161  itgsubst  26169  dgrco  26393  plyexmo  26435  ulmdvlem3  26523  abelthlem2  26553  abelthlem8  26560  mpodvdsmulf1o  27316  dvdsmulf1o  27318  chpchtsum  27341  dchrptlem2  27387  2sqlem5  27544  2sqlem9  27549  2sqb  27554  chpo1ubb  27603  vmadivsumb  27605  selbergb  27671  selberg2b  27674  selberg3lem2  27680  pntrsumbnd  27688  pntrlog2bnd  27706  pntibndlem3  27714  pnt3  27734  noresle  27819  nosupprefixmo  27822  noinfprefixmo  27823  nosupbday  27827  noinfbday  27842  noinfbnd1lem5  27849  addsprop  28127  mulsproplem9  28275  mulsasslem3  28316  expadds  28586  bdayfinbndlem1  28618  readdscl  28650  tgjustf  28700  hlcgreu  28845  mirreu3  28885  cgraswap  29072  cgracom  29074  cgratr  29075  flatcgra  29076  acopyeu  29086  brprlng  29123  axsegcon  29186  ax5seglem9  29196  axeuclid  29222  axcontlem10  29232  axcontlem12  29234  wwlksnredwwlkn0  30154  n4cyclfrgr  30551  frgrnbnb  30553  numclwwlk1lem2fo  30618  ablo4  30811  smcnlem  30958  pjhthmo  31563  pjpjpre  31680  lnconi  32294  resf1o  32987  mgcoval  33219  xrge0tsmsd  33306  erlval  33491  derangenlem  35534  pconnconn  35594  connpconn  35598  cvmfolem  35642  cvmliftmolem2  35645  cvmliftmo  35647  cvmliftlem7  35654  cvmlift2lem10  35675  cvmlift3lem8  35689  linecgr  36444  btwnconn1lem8  36457  btwnconn1lem14  36463  btwnconn3  36466  brsegle  36471  segletr  36477  segleantisym  36478  outsideofeq  36493  linethru  36516  finminlem  36691  nn0prpwlem  36695  neibastop2lem  36733  weiunpo  36838  mblfinlem3  38170  ftc1cnnc  38203  isbnd3  38295  cvlcvr1  39975  athgt  40092  4atlem12  40248  paddasslem12  40467  paddasslem13  40468  cdleme0cp  40850  cdleme42keg  41122  cdleme42mgN  41124  trlord  41205  cdlemg6c  41256  cdlemkid4  41570  dihopelvalcpre  41884  dihmeetlem1N  41926  dihglblem5apreN  41927  dihmeetlem4preN  41942  dihmeetlem6  41945  dihmeetlem10N  41952  dihmeetlem11N  41953  dihmeetlem13N  41955  dihjatcclem4  42057  fsuppssind  43187  prjspner1  43220  mzpcl1  43322  mzpcompact2lem  43344  diophin  43365  pell14qrmulcl  43452  pwssplit4  43678  hbtlem2  43713  iunrelexpuztr  44307  stoweidlem57  46629  stoweidlem61  46633  fourierdlem92  46770  euoreqb  47701  prproropf1olem3  48109  prproropf1olem4  48110  fpprwpprb  48360  cycldlenngric  48548  grimgrtri  48569  2zlidl  48860  lmodvsmdi  49010  2arwcat  50229