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  7228  mpo0  7438  fpr3g  8225  fprresex  8250  eroveu  8746  boxriin  8874  fofinf1o  9241  finsschain  9268  suppeqfsuppbi  9288  fsuppunbi  9298  marypha1lem  9342  wemapsolem  9461  wemapso  9462  wemapso2lem  9463  cantnf  9608  iunfictbso  10027  enfin2i  10234  ttukeylem7  10428  fpwwe2lem2  10545  fpwwe2lem8  10551  fpwwe2lem11  10554  fpwwelem  10558  distrlem4pr  10939  mulcmpblnr  10984  prsrlem1  10985  dedekind  11297  divdivdiv  11843  divmuleq  11847  divadddiv  11857  divsubdiv  11858  lediv12a  12036  xmullem  13184  xlemul1a  13208  seqcaopr  13964  leexp2r  14099  hashf1lem1  14380  hashf1lem2  14381  ccatsymb  14507  wrd2ind  14647  cshweqrep  14745  rtrclreclem4  14986  lo1le  15577  summolem2  15641  summo  15642  prodmolem2  15860  prodmo  15861  bezoutlem3  16470  bezoutlem4  16471  qredeu  16587  pcadd  16819  prmreclem2  16847  vdwlem9  16919  vdwlem10  16920  ramub1lem2  16957  ramub1  16958  prmgaplem7  16987  cofucl  17813  initoeu2  17941  setcmon  18012  poslubmo  18333  posglbmo  18334  rabsubmgmd  18596  issubmd  18698  grprcan  18870  isnsg3  19057  ghmpreima  19135  gaorber  19205  psgneu  19403  odcau  19501  lsmsubm  19550  lsmmod  19572  ablfaclem3  19986  rngpropd  20077  ringpropd  20191  lmodvsmmulgdi  20818  lmodprop2d  20845  lss1d  20884  lindff1  21745  islindf4  21763  assamulgscmlem2  21825  mplcoe1  21960  mplcoe5  21963  evlslem1  22005  mdetunilem7  22521  mdetunilem8  22522  mdetunilem9  22523  mdetuni0  22524  mdetmul  22526  cayhamlem3  22790  ppttop  22910  epttop  22912  cnhaus  23257  isreg2  23280  cncmp  23295  1stcfb  23348  2ndcomap  23361  1stccnp  23365  cldllycmp  23398  1stckgenlem  23456  txcls  23507  ptcnp  23525  txdis1cn  23538  txlly  23539  txnlly  23540  pthaus  23541  txhaus  23550  txkgen  23555  xkohaus  23556  xkococnlem  23562  xkococn  23563  opnfbas  23745  hausflimi  23883  hausflim  23884  hauspwpwf1  23890  alexsubALT  23954  tgpconncomp  24016  qustgplem  24024  metequiv2  24414  met2ndci  24426  nrmmetd  24478  nlmvscnlem1  24590  reconn  24733  xrge0tsms  24739  mulc1cncf  24814  ipcnlem1  25161  minveclem3  25345  pmltpc  25367  ovolicc2lem5  25438  ovolicc2  25439  uniioombllem6  25505  dyadmbllem  25516  vitalilem3  25527  mbfmullem  25642  itg2split  25666  itg2mono  25670  bddiblnc  25759  dvlip2  25916  lhop1  25935  dvcnvrelem1  25938  dvfsumrlim  25954  ftc1lem6  25964  itgsubst  25972  dgrco  26197  plyexmo  26237  ulmdvlem3  26327  abelthlem2  26358  abelthlem8  26365  mpodvdsmulf1o  27120  dvdsmulf1o  27122  chpchtsum  27146  dchrptlem2  27192  2sqlem5  27349  2sqlem9  27354  2sqb  27359  chpo1ubb  27408  vmadivsumb  27410  selbergb  27476  selberg2b  27479  selberg3lem2  27485  pntrsumbnd  27493  pntrlog2bnd  27511  pntibndlem3  27519  pnt3  27539  noresle  27625  nosupprefixmo  27628  noinfprefixmo  27629  nosupbday  27633  noinfbday  27648  noinfbnd1lem5  27655  addsprop  27906  mulsproplem9  28050  mulsasslem3  28091  expadds  28345  readdscl  28386  tgjustf  28436  hlcgreu  28581  mirreu3  28617  cgraswap  28783  cgracom  28785  cgratr  28786  flatcgra  28787  acopyeu  28797  axsegcon  28890  ax5seglem9  28900  axeuclid  28926  axcontlem10  28936  axcontlem12  28938  wwlksnredwwlkn0  29859  n4cyclfrgr  30253  frgrnbnb  30255  numclwwlk1lem2fo  30320  ablo4  30512  smcnlem  30659  pjhthmo  31264  pjpjpre  31381  lnconi  31995  resf1o  32686  mgcoval  32941  xrge0tsmsd  33028  erlval  33208  derangenlem  35143  pconnconn  35203  connpconn  35207  cvmfolem  35251  cvmliftmolem2  35254  cvmliftmo  35256  cvmliftlem7  35263  cvmlift2lem10  35284  cvmlift3lem8  35298  linecgr  36054  btwnconn1lem8  36067  btwnconn1lem14  36073  btwnconn3  36076  brsegle  36081  segletr  36087  segleantisym  36088  outsideofeq  36103  linethru  36126  finminlem  36291  nn0prpwlem  36295  neibastop2lem  36333  weiunpo  36438  mblfinlem3  37638  ftc1cnnc  37671  isbnd3  37763  cvlcvr1  39317  athgt  39435  4atlem12  39591  paddasslem12  39810  paddasslem13  39811  cdleme0cp  40193  cdleme42keg  40465  cdleme42mgN  40467  trlord  40548  cdlemg6c  40599  cdlemkid4  40913  dihopelvalcpre  41227  dihmeetlem1N  41269  dihglblem5apreN  41270  dihmeetlem4preN  41285  dihmeetlem6  41288  dihmeetlem10N  41295  dihmeetlem11N  41296  dihmeetlem13N  41298  dihjatcclem4  41400  fsuppssind  42566  prjspner1  42599  mzpcl1  42702  mzpcompact2lem  42724  diophin  42745  pell14qrmulcl  42836  pwssplit4  43062  hbtlem2  43097  iunrelexpuztr  43692  stoweidlem57  46039  stoweidlem61  46043  fourierdlem92  46180  euoreqb  47094  prproropf1olem3  47490  prproropf1olem4  47491  fpprwpprb  47725  cycldlenngric  47912  grimgrtri  47932  2zlidl  48212  lmodvsmdi  48351  2arwcat  49573