Theorem simprll 776

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  fcof1  7168  mpo0  7369  fpr3g  8110  fprresex  8135  wfrlem17OLD  8165  eroveu  8610  boxriin  8737  undomOLD  8856  fofinf1o  9103  finsschain  9135  suppeqfsuppbi  9151  fsuppunbi  9158  marypha1lem  9201  wemapsolem  9318  wemapso  9319  wemapso2lem  9320  cantnf  9460  iunfictbso  9879  enfin2i  10086  ttukeylem7  10280  fpwwe2lem2  10397  fpwwe2lem8  10403  fpwwe2lem11  10406  fpwwelem  10410  distrlem4pr  10791  mulcmpblnr  10836  prsrlem1  10837  dedekind  11147  divdivdiv  11685  divmuleq  11689  divadddiv  11699  divsubdiv  11700  lediv12a  11877  xmullem  13007  xlemul1a  13031  seqcaopr  13769  leexp2r  13901  hashf1lem1  14177  hashf1lem1OLD  14178  hashf1lem2  14179  ccatsymb  14296  wrd2ind  14445  cshweqrep  14543  rtrclreclem4  14781  lo1le  15372  summolem2  15437  summo  15438  prodmolem2  15654  prodmo  15655  bezoutlem3  16258  bezoutlem4  16259  qredeu  16372  pcadd  16599  prmreclem2  16627  vdwlem9  16699  vdwlem10  16700  ramub1lem2  16737  ramub1  16738  prmgaplem7  16767  cofucl  17612  initoeu2  17740  setcmon  17811  poslubmo  18138  posglbmo  18139  issubmd  18454  grprcan  18622  isnsg3  18797  ghmpreima  18865  gaorber  18923  psgneu  19123  odcau  19218  lsmsubm  19267  lsmmod  19290  ablfaclem3  19699  ringpropd  19830  lmodvsmmulgdi  20167  lmodprop2d  20194  lss1d  20234  lindff1  21036  islindf4  21054  assamulgscmlem2  21113  mplcoe1  21247  mplcoe5  21250  evlslem1  21301  mdetunilem7  21776  mdetunilem8  21777  mdetunilem9  21778  mdetuni0  21779  mdetmul  21781  cayhamlem3  22045  ppttop  22166  epttop  22168  cnhaus  22514  isreg2  22537  cncmp  22552  1stcfb  22605  2ndcomap  22618  1stccnp  22622  cldllycmp  22655  1stckgenlem  22713  txcls  22764  ptcnp  22782  txdis1cn  22795  txlly  22796  txnlly  22797  pthaus  22798  txhaus  22807  txkgen  22812  xkohaus  22813  xkococnlem  22819  xkococn  22820  opnfbas  23002  hausflimi  23140  hausflim  23141  hauspwpwf1  23147  alexsubALT  23211  tgpconncomp  23273  qustgplem  23281  metequiv2  23675  met2ndci  23687  nrmmetd  23739  nlmvscnlem1  23859  reconn  24000  xrge0tsms  24006  mulc1cncf  24077  ipcnlem1  24418  minveclem3  24602  pmltpc  24623  ovolicc2lem5  24694  ovolicc2  24695  uniioombllem6  24761  dyadmbllem  24772  vitalilem3  24783  mbfmullem  24899  itg2split  24923  itg2mono  24927  bddiblnc  25015  dvlip2  25168  lhop1  25187  dvcnvrelem1  25190  dvfsumrlim  25204  ftc1lem6  25214  itgsubst  25222  dgrco  25445  plyexmo  25482  ulmdvlem3  25570  abelthlem2  25600  abelthlem8  25607  dvdsmulf1o  26352  chpchtsum  26376  dchrptlem2  26422  2sqlem5  26579  2sqlem9  26584  2sqb  26589  chpo1ubb  26638  vmadivsumb  26640  selbergb  26706  selberg2b  26709  selberg3lem2  26715  pntrsumbnd  26723  pntrlog2bnd  26741  pntibndlem3  26749  pnt3  26769  tgjustf  26843  hlcgreu  26988  mirreu3  27024  cgraswap  27190  cgracom  27192  cgratr  27193  flatcgra  27194  acopyeu  27204  axsegcon  27304  ax5seglem9  27314  axeuclid  27340  axcontlem10  27350  axcontlem12  27352  wwlksnredwwlkn0  28270  n4cyclfrgr  28664  frgrnbnb  28666  numclwwlk1lem2fo  28731  ablo4  28921  smcnlem  29068  pjhthmo  29673  pjpjpre  29790  lnconi  30404  resf1o  31074  mgcoval  31273  xrge0tsmsd  31326  derangenlem  33142  pconnconn  33202  connpconn  33206  cvmfolem  33250  cvmliftmolem2  33253  cvmliftmo  33255  cvmliftlem7  33262  cvmlift2lem10  33283  cvmlift3lem8  33297  noresle  33909  nosupprefixmo  33912  noinfprefixmo  33913  nosupbday  33917  noinfbday  33932  noinfbnd1lem5  33939  linecgr  34392  btwnconn1lem8  34405  btwnconn1lem14  34411  btwnconn3  34414  brsegle  34419  segletr  34425  segleantisym  34426  outsideofeq  34441  linethru  34464  finminlem  34516  nn0prpwlem  34520  neibastop2lem  34558  mblfinlem3  35825  ftc1cnnc  35858  isbnd3  35951  cvlcvr1  37360  athgt  37477  4atlem12  37633  paddasslem12  37852  paddasslem13  37853  cdleme0cp  38235  cdleme42keg  38507  cdleme42mgN  38509  trlord  38590  cdlemg6c  38641  cdlemkid4  38955  dihopelvalcpre  39269  dihmeetlem1N  39311  dihglblem5apreN  39312  dihmeetlem4preN  39327  dihmeetlem6  39330  dihmeetlem10N  39337  dihmeetlem11N  39338  dihmeetlem13N  39340  dihjatcclem4  39442  fsuppssind  40289  prjspner1  40470  mzpcl1  40558  mzpcompact2lem  40580  diophin  40601  pell14qrmulcl  40692  pwssplit4  40921  hbtlem2  40956  iunrelexpuztr  41334  stoweidlem57  43605  stoweidlem61  43609  fourierdlem92  43746  euoreqb  44612  prproropf1olem3  44968  prproropf1olem4  44969  fpprwpprb  45203  rabsubmgmd  45356  2zlidl  45503  lmodvsmdi  45729