Theorem simprll 802

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 473	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrl 764	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  disjxiunOLD  4650  fcof1  6542  mpt20  6725  wfrlem17  7431  eroveu  7842  boxriin  7950  undom  8048  fofinf1o  8241  finsschain  8273  suppeqfsuppbi  8289  fsuppunbi  8296  marypha1lem  8339  wemapsolem  8455  wemapso  8456  wemapso2lem  8457  cantnf  8590  iunfictbso  8937  enfin2i  9143  ttukeylem7  9337  fpwwe2lem2  9454  fpwwe2lem9  9460  fpwwe2lem12  9463  fpwwelem  9467  distrlem4pr  9848  mulcmpblnr  9892  prsrlem1  9893  dedekind  10200  divdivdiv  10726  divmuleq  10730  divadddiv  10740  divsubdiv  10741  lediv12a  10916  xmullem  12094  xlemul1a  12118  seqcaopr  12838  leexp2r  12918  hashf1lem1  13239  hashf1lem2  13240  wrd2ind  13477  cshweqrep  13567  lo1le  14382  summolem2  14447  summo  14448  prodmolem2  14665  prodmo  14666  bezoutlem3  15258  bezoutlem4  15259  qredeu  15372  pcadd  15593  prmreclem2  15621  vdwlem9  15693  vdwlem10  15694  ramub1lem2  15731  ramub1  15732  prmgaplem7  15761  cofucl  16548  setcmon  16737  poslubmo  17146  posglbmo  17147  issubmd  17349  grprcan  17455  isnsg3  17628  ghmpreima  17682  gaorber  17741  psgneu  17926  odcau  18019  lsmsubm  18068  lsmmod  18088  ablfaclem3  18486  ringpropd  18582  lmodvsmmulgdi  18898  lmodprop2d  18925  lss1d  18963  assamulgscmlem2  19349  mplcoe1  19465  mplcoe5  19468  evlslem1  19515  lindff1  20159  islindf4  20177  mdetunilem7  20424  mdetunilem8  20425  mdetunilem9  20426  mdetuni0  20427  mdetmul  20429  cayhamlem3  20692  ppttop  20811  epttop  20813  cnhaus  21158  isreg2  21181  cncmp  21195  1stcfb  21248  2ndcomap  21261  1stccnp  21265  cldllycmp  21298  1stckgenlem  21356  txcls  21407  ptcnp  21425  txdis1cn  21438  txlly  21439  txnlly  21440  pthaus  21441  txhaus  21450  txkgen  21455  xkohaus  21456  xkococnlem  21462  xkococn  21463  opnfbas  21646  hausflimi  21784  hausflim  21785  hauspwpwf1  21791  alexsubALT  21855  tgpconncomp  21916  qustgplem  21924  metequiv2  22315  met2ndci  22327  nrmmetd  22379  nlmvscnlem1  22490  reconn  22631  xrge0tsms  22637  mulc1cncf  22708  ipcnlem1  23044  minveclem3  23200  pmltpc  23219  ovolicc2lem5  23289  ovolicc2  23290  uniioombllem6  23356  dyadmbllem  23367  vitalilem3  23379  mbfmullem  23492  itg2split  23516  itg2mono  23520  dvlip2  23758  lhop1  23777  dvcnvrelem1  23780  dvfsumrlim  23794  ftc1lem6  23804  itgsubst  23812  dgrco  24031  plyexmo  24068  ulmdvlem3  24156  abelthlem2  24186  abelthlem8  24193  dvdsmulf1o  24920  chpchtsum  24944  dchrptlem2  24990  2sqlem5  25147  2sqlem9  25152  2sqb  25157  chpo1ubb  25170  vmadivsumb  25172  selbergb  25238  selberg2b  25241  selberg3lem2  25247  pntrsumbnd  25255  pntrlog2bnd  25273  pntibndlem3  25281  pnt3  25301  hlcgreu  25513  mirreu3  25549  cgraswap  25712  cgracom  25714  cgratr  25715  acopyeu  25725  axsegcon  25807  ax5seglem9  25817  axeuclid  25843  axcontlem10  25853  axcontlem12  25855  wwlksnredwwlkn0  26791  frgrnbnb  27157  numclwlk1lem2f1  27227  numclwlk1lem2fo  27228  ablo4  27404  smcnlem  27552  pjhthmo  28161  pjpjpre  28278  lnconi  28892  resf1o  29505  xrge0tsmsd  29785  derangenlem  31153  pconnconn  31213  connpconn  31217  cvmfolem  31261  cvmliftmolem2  31264  cvmliftmo  31266  cvmliftlem7  31273  cvmlift2lem10  31294  cvmlift3lem8  31308  noresle  31846  linecgr  32188  btwnconn1lem8  32201  btwnconn1lem14  32207  btwnconn3  32210  brsegle  32215  segletr  32221  segleantisym  32222  outsideofeq  32237  linethru  32260  finminlem  32312  nn0prpwlem  32317  neibastop2lem  32355  mblfinlem3  33448  bddiblnc  33480  ftc1cnnc  33484  isbnd3  33583  cvlcvr1  34626  athgt  34742  4atlem12  34898  paddasslem12  35117  paddasslem13  35118  cdleme0cp  35501  cdleme42keg  35774  cdleme42mgN  35776  trlord  35857  cdlemg6c  35908  cdlemkid4  36222  dihopelvalcpre  36537  dihmeetlem1N  36579  dihglblem5apreN  36580  dihmeetlem4preN  36595  dihmeetlem6  36598  dihmeetlem10N  36605  dihmeetlem11N  36606  dihmeetlem13N  36608  dihjatcclem4  36710  mzpcl1  37292  mzpcompact2lem  37314  diophin  37336  pell14qrmulcl  37427  pwssplit4  37659  hbtlem2  37694  iunrelexpuztr  38011  stoweidlem57  40274  stoweidlem61  40278  fourierdlem92  40415  rabsubmgmd  41791  2zlidl  41934  lmodvsmdi  42163