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 727	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  7323  mpo0  7535  fpr3g  8326  fprresex  8351  wfrlem17OLD  8381  eroveu  8870  boxriin  8998  undomOLD  9126  fofinf1o  9400  finsschain  9429  suppeqfsuppbi  9448  fsuppunbi  9458  marypha1lem  9502  wemapsolem  9619  wemapso  9620  wemapso2lem  9621  cantnf  9762  iunfictbso  10183  enfin2i  10390  ttukeylem7  10584  fpwwe2lem2  10701  fpwwe2lem8  10707  fpwwe2lem11  10710  fpwwelem  10714  distrlem4pr  11095  mulcmpblnr  11140  prsrlem1  11141  dedekind  11453  divdivdiv  11995  divmuleq  11999  divadddiv  12009  divsubdiv  12010  lediv12a  12188  xmullem  13326  xlemul1a  13350  seqcaopr  14090  leexp2r  14224  hashf1lem1  14504  hashf1lem2  14505  ccatsymb  14630  wrd2ind  14771  cshweqrep  14869  rtrclreclem4  15110  lo1le  15700  summolem2  15764  summo  15765  prodmolem2  15983  prodmo  15984  bezoutlem3  16588  bezoutlem4  16589  qredeu  16705  pcadd  16936  prmreclem2  16964  vdwlem9  17036  vdwlem10  17037  ramub1lem2  17074  ramub1  17075  prmgaplem7  17104  cofucl  17952  initoeu2  18083  setcmon  18154  poslubmo  18481  posglbmo  18482  rabsubmgmd  18742  issubmd  18841  grprcan  19013  isnsg3  19200  ghmpreima  19278  gaorber  19348  psgneu  19548  odcau  19646  lsmsubm  19695  lsmmod  19717  ablfaclem3  20131  rngpropd  20201  ringpropd  20311  lmodvsmmulgdi  20917  lmodprop2d  20944  lss1d  20984  lindff1  21863  islindf4  21881  assamulgscmlem2  21943  mplcoe1  22078  mplcoe5  22081  evlslem1  22129  mdetunilem7  22645  mdetunilem8  22646  mdetunilem9  22647  mdetuni0  22648  mdetmul  22650  cayhamlem3  22914  ppttop  23035  epttop  23037  cnhaus  23383  isreg2  23406  cncmp  23421  1stcfb  23474  2ndcomap  23487  1stccnp  23491  cldllycmp  23524  1stckgenlem  23582  txcls  23633  ptcnp  23651  txdis1cn  23664  txlly  23665  txnlly  23666  pthaus  23667  txhaus  23676  txkgen  23681  xkohaus  23682  xkococnlem  23688  xkococn  23689  opnfbas  23871  hausflimi  24009  hausflim  24010  hauspwpwf1  24016  alexsubALT  24080  tgpconncomp  24142  qustgplem  24150  metequiv2  24544  met2ndci  24556  nrmmetd  24608  nlmvscnlem1  24728  reconn  24869  xrge0tsms  24875  mulc1cncf  24950  ipcnlem1  25298  minveclem3  25482  pmltpc  25504  ovolicc2lem5  25575  ovolicc2  25576  uniioombllem6  25642  dyadmbllem  25653  vitalilem3  25664  mbfmullem  25780  itg2split  25804  itg2mono  25808  bddiblnc  25897  dvlip2  26054  lhop1  26073  dvcnvrelem1  26076  dvfsumrlim  26092  ftc1lem6  26102  itgsubst  26110  dgrco  26335  plyexmo  26373  ulmdvlem3  26463  abelthlem2  26494  abelthlem8  26501  mpodvdsmulf1o  27255  dvdsmulf1o  27257  chpchtsum  27281  dchrptlem2  27327  2sqlem5  27484  2sqlem9  27489  2sqb  27494  chpo1ubb  27543  vmadivsumb  27545  selbergb  27611  selberg2b  27614  selberg3lem2  27620  pntrsumbnd  27628  pntrlog2bnd  27646  pntibndlem3  27654  pnt3  27674  noresle  27760  nosupprefixmo  27763  noinfprefixmo  27764  nosupbday  27768  noinfbday  27783  noinfbnd1lem5  27790  addsprop  28027  mulsproplem9  28168  mulsasslem3  28209  readdscl  28449  tgjustf  28499  hlcgreu  28644  mirreu3  28680  cgraswap  28846  cgracom  28848  cgratr  28849  flatcgra  28850  acopyeu  28860  axsegcon  28960  ax5seglem9  28970  axeuclid  28996  axcontlem10  29006  axcontlem12  29008  wwlksnredwwlkn0  29929  n4cyclfrgr  30323  frgrnbnb  30325  numclwwlk1lem2fo  30390  ablo4  30582  smcnlem  30729  pjhthmo  31334  pjpjpre  31451  lnconi  32065  resf1o  32744  mgcoval  32959  xrge0tsmsd  33041  erlval  33230  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  36284  nn0prpwlem  36288  neibastop2lem  36326  weiunpo  36431  mblfinlem3  37619  ftc1cnnc  37652  isbnd3  37744  cvlcvr1  39295  athgt  39413  4atlem12  39569  paddasslem12  39788  paddasslem13  39789  cdleme0cp  40171  cdleme42keg  40443  cdleme42mgN  40445  trlord  40526  cdlemg6c  40577  cdlemkid4  40891  dihopelvalcpre  41205  dihmeetlem1N  41247  dihglblem5apreN  41248  dihmeetlem4preN  41263  dihmeetlem6  41266  dihmeetlem10N  41273  dihmeetlem11N  41274  dihmeetlem13N  41276  dihjatcclem4  41378  fsuppssind  42548  prjspner1  42581  mzpcl1  42685  mzpcompact2lem  42707  diophin  42728  pell14qrmulcl  42819  pwssplit4  43046  hbtlem2  43081  iunrelexpuztr  43681  stoweidlem57  45978  stoweidlem61  45982  fourierdlem92  46119  euoreqb  47024  prproropf1olem3  47379  prproropf1olem4  47380  fpprwpprb  47614  grimgrtri  47798  2zlidl  47963  lmodvsmdi  48107