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  7265  mpo0  7477  fpr3g  8267  fprresex  8292  eroveu  8788  boxriin  8916  undomOLD  9034  fofinf1o  9290  finsschain  9317  suppeqfsuppbi  9337  fsuppunbi  9347  marypha1lem  9391  wemapsolem  9510  wemapso  9511  wemapso2lem  9512  cantnf  9653  iunfictbso  10074  enfin2i  10281  ttukeylem7  10475  fpwwe2lem2  10592  fpwwe2lem8  10598  fpwwe2lem11  10601  fpwwelem  10605  distrlem4pr  10986  mulcmpblnr  11031  prsrlem1  11032  dedekind  11344  divdivdiv  11890  divmuleq  11894  divadddiv  11904  divsubdiv  11905  lediv12a  12083  xmullem  13231  xlemul1a  13255  seqcaopr  14011  leexp2r  14146  hashf1lem1  14427  hashf1lem2  14428  ccatsymb  14554  wrd2ind  14695  cshweqrep  14793  rtrclreclem4  15034  lo1le  15625  summolem2  15689  summo  15690  prodmolem2  15908  prodmo  15909  bezoutlem3  16518  bezoutlem4  16519  qredeu  16635  pcadd  16867  prmreclem2  16895  vdwlem9  16967  vdwlem10  16968  ramub1lem2  17005  ramub1  17006  prmgaplem7  17035  cofucl  17857  initoeu2  17985  setcmon  18056  poslubmo  18377  posglbmo  18378  rabsubmgmd  18638  issubmd  18740  grprcan  18912  isnsg3  19099  ghmpreima  19177  gaorber  19247  psgneu  19443  odcau  19541  lsmsubm  19590  lsmmod  19612  ablfaclem3  20026  rngpropd  20090  ringpropd  20204  lmodvsmmulgdi  20810  lmodprop2d  20837  lss1d  20876  lindff1  21736  islindf4  21754  assamulgscmlem2  21816  mplcoe1  21951  mplcoe5  21954  evlslem1  21996  mdetunilem7  22512  mdetunilem8  22513  mdetunilem9  22514  mdetuni0  22515  mdetmul  22517  cayhamlem3  22781  ppttop  22901  epttop  22903  cnhaus  23248  isreg2  23271  cncmp  23286  1stcfb  23339  2ndcomap  23352  1stccnp  23356  cldllycmp  23389  1stckgenlem  23447  txcls  23498  ptcnp  23516  txdis1cn  23529  txlly  23530  txnlly  23531  pthaus  23532  txhaus  23541  txkgen  23546  xkohaus  23547  xkococnlem  23553  xkococn  23554  opnfbas  23736  hausflimi  23874  hausflim  23875  hauspwpwf1  23881  alexsubALT  23945  tgpconncomp  24007  qustgplem  24015  metequiv2  24405  met2ndci  24417  nrmmetd  24469  nlmvscnlem1  24581  reconn  24724  xrge0tsms  24730  mulc1cncf  24805  ipcnlem1  25152  minveclem3  25336  pmltpc  25358  ovolicc2lem5  25429  ovolicc2  25430  uniioombllem6  25496  dyadmbllem  25507  vitalilem3  25518  mbfmullem  25633  itg2split  25657  itg2mono  25661  bddiblnc  25750  dvlip2  25907  lhop1  25926  dvcnvrelem1  25929  dvfsumrlim  25945  ftc1lem6  25955  itgsubst  25963  dgrco  26188  plyexmo  26228  ulmdvlem3  26318  abelthlem2  26349  abelthlem8  26356  mpodvdsmulf1o  27111  dvdsmulf1o  27113  chpchtsum  27137  dchrptlem2  27183  2sqlem5  27340  2sqlem9  27345  2sqb  27350  chpo1ubb  27399  vmadivsumb  27401  selbergb  27467  selberg2b  27470  selberg3lem2  27476  pntrsumbnd  27484  pntrlog2bnd  27502  pntibndlem3  27510  pnt3  27530  noresle  27616  nosupprefixmo  27619  noinfprefixmo  27620  nosupbday  27624  noinfbday  27639  noinfbnd1lem5  27646  addsprop  27890  mulsproplem9  28034  mulsasslem3  28075  expadds  28327  readdscl  28357  tgjustf  28407  hlcgreu  28552  mirreu3  28588  cgraswap  28754  cgracom  28756  cgratr  28757  flatcgra  28758  acopyeu  28768  axsegcon  28861  ax5seglem9  28871  axeuclid  28897  axcontlem10  28907  axcontlem12  28909  wwlksnredwwlkn0  29833  n4cyclfrgr  30227  frgrnbnb  30229  numclwwlk1lem2fo  30294  ablo4  30486  smcnlem  30633  pjhthmo  31238  pjpjpre  31355  lnconi  31969  resf1o  32660  mgcoval  32919  xrge0tsmsd  33009  erlval  33216  derangenlem  35165  pconnconn  35225  connpconn  35229  cvmfolem  35273  cvmliftmolem2  35276  cvmliftmo  35278  cvmliftlem7  35285  cvmlift2lem10  35306  cvmlift3lem8  35320  linecgr  36076  btwnconn1lem8  36089  btwnconn1lem14  36095  btwnconn3  36098  brsegle  36103  segletr  36109  segleantisym  36110  outsideofeq  36125  linethru  36148  finminlem  36313  nn0prpwlem  36317  neibastop2lem  36355  weiunpo  36460  mblfinlem3  37660  ftc1cnnc  37693  isbnd3  37785  cvlcvr1  39339  athgt  39457  4atlem12  39613  paddasslem12  39832  paddasslem13  39833  cdleme0cp  40215  cdleme42keg  40487  cdleme42mgN  40489  trlord  40570  cdlemg6c  40621  cdlemkid4  40935  dihopelvalcpre  41249  dihmeetlem1N  41291  dihglblem5apreN  41292  dihmeetlem4preN  41307  dihmeetlem6  41310  dihmeetlem10N  41317  dihmeetlem11N  41318  dihmeetlem13N  41320  dihjatcclem4  41422  fsuppssind  42588  prjspner1  42621  mzpcl1  42724  mzpcompact2lem  42746  diophin  42767  pell14qrmulcl  42858  pwssplit4  43085  hbtlem2  43120  iunrelexpuztr  43715  stoweidlem57  46062  stoweidlem61  46066  fourierdlem92  46203  euoreqb  47114  prproropf1olem3  47510  prproropf1olem4  47511  fpprwpprb  47745  cycldlenngric  47932  grimgrtri  47952  2zlidl  48232  lmodvsmdi  48371  2arwcat  49593