Theorem simprll 779

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  7306  mpo0  7517  fpr3g  8308  fprresex  8333  wfrlem17OLD  8363  eroveu  8850  boxriin  8978  undomOLD  9098  fofinf1o  9369  finsschain  9396  suppeqfsuppbi  9416  fsuppunbi  9426  marypha1lem  9470  wemapsolem  9587  wemapso  9588  wemapso2lem  9589  cantnf  9730  iunfictbso  10151  enfin2i  10358  ttukeylem7  10552  fpwwe2lem2  10669  fpwwe2lem8  10675  fpwwe2lem11  10678  fpwwelem  10682  distrlem4pr  11063  mulcmpblnr  11108  prsrlem1  11109  dedekind  11421  divdivdiv  11965  divmuleq  11969  divadddiv  11979  divsubdiv  11980  lediv12a  12158  xmullem  13302  xlemul1a  13326  seqcaopr  14076  leexp2r  14210  hashf1lem1  14490  hashf1lem2  14491  ccatsymb  14616  wrd2ind  14757  cshweqrep  14855  rtrclreclem4  15096  lo1le  15684  summolem2  15748  summo  15749  prodmolem2  15967  prodmo  15968  bezoutlem3  16574  bezoutlem4  16575  qredeu  16691  pcadd  16922  prmreclem2  16950  vdwlem9  17022  vdwlem10  17023  ramub1lem2  17060  ramub1  17061  prmgaplem7  17090  cofucl  17938  initoeu2  18069  setcmon  18140  poslubmo  18468  posglbmo  18469  rabsubmgmd  18729  issubmd  18831  grprcan  19003  isnsg3  19190  ghmpreima  19268  gaorber  19338  psgneu  19538  odcau  19636  lsmsubm  19685  lsmmod  19707  ablfaclem3  20121  rngpropd  20191  ringpropd  20301  lmodvsmmulgdi  20911  lmodprop2d  20938  lss1d  20978  lindff1  21857  islindf4  21875  assamulgscmlem2  21937  mplcoe1  22072  mplcoe5  22075  evlslem1  22123  mdetunilem7  22639  mdetunilem8  22640  mdetunilem9  22641  mdetuni0  22642  mdetmul  22644  cayhamlem3  22908  ppttop  23029  epttop  23031  cnhaus  23377  isreg2  23400  cncmp  23415  1stcfb  23468  2ndcomap  23481  1stccnp  23485  cldllycmp  23518  1stckgenlem  23576  txcls  23627  ptcnp  23645  txdis1cn  23658  txlly  23659  txnlly  23660  pthaus  23661  txhaus  23670  txkgen  23675  xkohaus  23676  xkococnlem  23682  xkococn  23683  opnfbas  23865  hausflimi  24003  hausflim  24004  hauspwpwf1  24010  alexsubALT  24074  tgpconncomp  24136  qustgplem  24144  metequiv2  24538  met2ndci  24550  nrmmetd  24602  nlmvscnlem1  24722  reconn  24863  xrge0tsms  24869  mulc1cncf  24944  ipcnlem1  25292  minveclem3  25476  pmltpc  25498  ovolicc2lem5  25569  ovolicc2  25570  uniioombllem6  25636  dyadmbllem  25647  vitalilem3  25658  mbfmullem  25774  itg2split  25798  itg2mono  25802  bddiblnc  25891  dvlip2  26048  lhop1  26067  dvcnvrelem1  26070  dvfsumrlim  26086  ftc1lem6  26096  itgsubst  26104  dgrco  26329  plyexmo  26369  ulmdvlem3  26459  abelthlem2  26490  abelthlem8  26497  mpodvdsmulf1o  27251  dvdsmulf1o  27253  chpchtsum  27277  dchrptlem2  27323  2sqlem5  27480  2sqlem9  27485  2sqb  27490  chpo1ubb  27539  vmadivsumb  27541  selbergb  27607  selberg2b  27610  selberg3lem2  27616  pntrsumbnd  27624  pntrlog2bnd  27642  pntibndlem3  27650  pnt3  27670  noresle  27756  nosupprefixmo  27759  noinfprefixmo  27760  nosupbday  27764  noinfbday  27779  noinfbnd1lem5  27786  addsprop  28023  mulsproplem9  28164  mulsasslem3  28205  readdscl  28445  tgjustf  28495  hlcgreu  28640  mirreu3  28676  cgraswap  28842  cgracom  28844  cgratr  28845  flatcgra  28846  acopyeu  28856  axsegcon  28956  ax5seglem9  28966  axeuclid  28992  axcontlem10  29002  axcontlem12  29004  wwlksnredwwlkn0  29925  n4cyclfrgr  30319  frgrnbnb  30321  numclwwlk1lem2fo  30386  ablo4  30578  smcnlem  30725  pjhthmo  31330  pjpjpre  31447  lnconi  32061  resf1o  32747  mgcoval  32960  xrge0tsmsd  33047  erlval  33244  derangenlem  35155  pconnconn  35215  connpconn  35219  cvmfolem  35263  cvmliftmolem2  35266  cvmliftmo  35268  cvmliftlem7  35275  cvmlift2lem10  35296  cvmlift3lem8  35310  linecgr  36062  btwnconn1lem8  36075  btwnconn1lem14  36081  btwnconn3  36084  brsegle  36089  segletr  36095  segleantisym  36096  outsideofeq  36111  linethru  36134  finminlem  36300  nn0prpwlem  36304  neibastop2lem  36342  weiunpo  36447  mblfinlem3  37645  ftc1cnnc  37678  isbnd3  37770  cvlcvr1  39320  athgt  39438  4atlem12  39594  paddasslem12  39813  paddasslem13  39814  cdleme0cp  40196  cdleme42keg  40468  cdleme42mgN  40470  trlord  40551  cdlemg6c  40602  cdlemkid4  40916  dihopelvalcpre  41230  dihmeetlem1N  41272  dihglblem5apreN  41273  dihmeetlem4preN  41288  dihmeetlem6  41291  dihmeetlem10N  41298  dihmeetlem11N  41299  dihmeetlem13N  41301  dihjatcclem4  41403  fsuppssind  42579  prjspner1  42612  mzpcl1  42716  mzpcompact2lem  42738  diophin  42759  pell14qrmulcl  42850  pwssplit4  43077  hbtlem2  43112  iunrelexpuztr  43708  stoweidlem57  46012  stoweidlem61  46016  fourierdlem92  46153  euoreqb  47058  prproropf1olem3  47429  prproropf1olem4  47430  fpprwpprb  47664  grimgrtri  47851  2zlidl  48083  lmodvsmdi  48223