Theorem simprll 778

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 482	. 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  7279  mpo0  7490  fpr3g  8282  fprresex  8307  wfrlem17OLD  8337  eroveu  8824  boxriin  8952  undomOLD  9072  fofinf1o  9342  finsschain  9369  suppeqfsuppbi  9389  fsuppunbi  9399  marypha1lem  9443  wemapsolem  9562  wemapso  9563  wemapso2lem  9564  cantnf  9705  iunfictbso  10126  enfin2i  10333  ttukeylem7  10527  fpwwe2lem2  10644  fpwwe2lem8  10650  fpwwe2lem11  10653  fpwwelem  10657  distrlem4pr  11038  mulcmpblnr  11083  prsrlem1  11084  dedekind  11396  divdivdiv  11940  divmuleq  11944  divadddiv  11954  divsubdiv  11955  lediv12a  12133  xmullem  13278  xlemul1a  13302  seqcaopr  14055  leexp2r  14190  hashf1lem1  14471  hashf1lem2  14472  ccatsymb  14598  wrd2ind  14739  cshweqrep  14837  rtrclreclem4  15078  lo1le  15666  summolem2  15730  summo  15731  prodmolem2  15949  prodmo  15950  bezoutlem3  16558  bezoutlem4  16559  qredeu  16675  pcadd  16907  prmreclem2  16935  vdwlem9  17007  vdwlem10  17008  ramub1lem2  17045  ramub1  17046  prmgaplem7  17075  cofucl  17899  initoeu2  18027  setcmon  18098  poslubmo  18419  posglbmo  18420  rabsubmgmd  18680  issubmd  18782  grprcan  18954  isnsg3  19141  ghmpreima  19219  gaorber  19289  psgneu  19485  odcau  19583  lsmsubm  19632  lsmmod  19654  ablfaclem3  20068  rngpropd  20132  ringpropd  20246  lmodvsmmulgdi  20852  lmodprop2d  20879  lss1d  20918  lindff1  21778  islindf4  21796  assamulgscmlem2  21858  mplcoe1  21993  mplcoe5  21996  evlslem1  22038  mdetunilem7  22554  mdetunilem8  22555  mdetunilem9  22556  mdetuni0  22557  mdetmul  22559  cayhamlem3  22823  ppttop  22943  epttop  22945  cnhaus  23290  isreg2  23313  cncmp  23328  1stcfb  23381  2ndcomap  23394  1stccnp  23398  cldllycmp  23431  1stckgenlem  23489  txcls  23540  ptcnp  23558  txdis1cn  23571  txlly  23572  txnlly  23573  pthaus  23574  txhaus  23583  txkgen  23588  xkohaus  23589  xkococnlem  23595  xkococn  23596  opnfbas  23778  hausflimi  23916  hausflim  23917  hauspwpwf1  23923  alexsubALT  23987  tgpconncomp  24049  qustgplem  24057  metequiv2  24447  met2ndci  24459  nrmmetd  24511  nlmvscnlem1  24623  reconn  24766  xrge0tsms  24772  mulc1cncf  24847  ipcnlem1  25195  minveclem3  25379  pmltpc  25401  ovolicc2lem5  25472  ovolicc2  25473  uniioombllem6  25539  dyadmbllem  25550  vitalilem3  25561  mbfmullem  25676  itg2split  25700  itg2mono  25704  bddiblnc  25793  dvlip2  25950  lhop1  25969  dvcnvrelem1  25972  dvfsumrlim  25988  ftc1lem6  25998  itgsubst  26006  dgrco  26231  plyexmo  26271  ulmdvlem3  26361  abelthlem2  26392  abelthlem8  26399  mpodvdsmulf1o  27154  dvdsmulf1o  27156  chpchtsum  27180  dchrptlem2  27226  2sqlem5  27383  2sqlem9  27388  2sqb  27393  chpo1ubb  27442  vmadivsumb  27444  selbergb  27510  selberg2b  27513  selberg3lem2  27519  pntrsumbnd  27527  pntrlog2bnd  27545  pntibndlem3  27553  pnt3  27573  noresle  27659  nosupprefixmo  27662  noinfprefixmo  27663  nosupbday  27667  noinfbday  27682  noinfbnd1lem5  27689  addsprop  27926  mulsproplem9  28067  mulsasslem3  28108  readdscl  28348  tgjustf  28398  hlcgreu  28543  mirreu3  28579  cgraswap  28745  cgracom  28747  cgratr  28748  flatcgra  28749  acopyeu  28759  axsegcon  28852  ax5seglem9  28862  axeuclid  28888  axcontlem10  28898  axcontlem12  28900  wwlksnredwwlkn0  29824  n4cyclfrgr  30218  frgrnbnb  30220  numclwwlk1lem2fo  30285  ablo4  30477  smcnlem  30624  pjhthmo  31229  pjpjpre  31346  lnconi  31960  resf1o  32653  mgcoval  32912  xrge0tsmsd  33002  erlval  33199  derangenlem  35139  pconnconn  35199  connpconn  35203  cvmfolem  35247  cvmliftmolem2  35250  cvmliftmo  35252  cvmliftlem7  35259  cvmlift2lem10  35280  cvmlift3lem8  35294  linecgr  36045  btwnconn1lem8  36058  btwnconn1lem14  36064  btwnconn3  36067  brsegle  36072  segletr  36078  segleantisym  36079  outsideofeq  36094  linethru  36117  finminlem  36282  nn0prpwlem  36286  neibastop2lem  36324  weiunpo  36429  mblfinlem3  37629  ftc1cnnc  37662  isbnd3  37754  cvlcvr1  39303  athgt  39421  4atlem12  39577  paddasslem12  39796  paddasslem13  39797  cdleme0cp  40179  cdleme42keg  40451  cdleme42mgN  40453  trlord  40534  cdlemg6c  40585  cdlemkid4  40899  dihopelvalcpre  41213  dihmeetlem1N  41255  dihglblem5apreN  41256  dihmeetlem4preN  41271  dihmeetlem6  41274  dihmeetlem10N  41281  dihmeetlem11N  41282  dihmeetlem13N  41284  dihjatcclem4  41386  fsuppssind  42563  prjspner1  42596  mzpcl1  42699  mzpcompact2lem  42721  diophin  42742  pell14qrmulcl  42833  pwssplit4  43060  hbtlem2  43095  iunrelexpuztr  43690  stoweidlem57  46034  stoweidlem61  46038  fourierdlem92  46175  euoreqb  47086  prproropf1olem3  47467  prproropf1olem4  47468  fpprwpprb  47702  cycldlenngric  47889  grimgrtri  47909  2zlidl  48163  lmodvsmdi  48302  2arwcat  49425