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  7216  mpo0  7426  fpr3g  8210  fprresex  8235  eroveu  8731  boxriin  8859  fofinf1o  9211  finsschain  9238  suppeqfsuppbi  9258  fsuppunbi  9268  marypha1lem  9312  wemapsolem  9431  wemapso  9432  wemapso2lem  9433  cantnf  9578  iunfictbso  9997  enfin2i  10204  ttukeylem7  10398  fpwwe2lem2  10515  fpwwe2lem8  10521  fpwwe2lem11  10524  fpwwelem  10528  distrlem4pr  10909  mulcmpblnr  10954  prsrlem1  10955  dedekind  11268  divdivdiv  11814  divmuleq  11818  divadddiv  11828  divsubdiv  11829  lediv12a  12007  xmullem  13155  xlemul1a  13179  seqcaopr  13938  leexp2r  14073  hashf1lem1  14354  hashf1lem2  14355  ccatsymb  14482  wrd2ind  14622  cshweqrep  14720  rtrclreclem4  14960  lo1le  15551  summolem2  15615  summo  15616  prodmolem2  15834  prodmo  15835  bezoutlem3  16444  bezoutlem4  16445  qredeu  16561  pcadd  16793  prmreclem2  16821  vdwlem9  16893  vdwlem10  16894  ramub1lem2  16931  ramub1  16932  prmgaplem7  16961  cofucl  17787  initoeu2  17915  setcmon  17986  poslubmo  18307  posglbmo  18308  rabsubmgmd  18604  issubmd  18706  grprcan  18878  isnsg3  19065  ghmpreima  19143  gaorber  19213  psgneu  19411  odcau  19509  lsmsubm  19558  lsmmod  19580  ablfaclem3  19994  rngpropd  20085  ringpropd  20199  lmodvsmmulgdi  20823  lmodprop2d  20850  lss1d  20889  lindff1  21750  islindf4  21768  assamulgscmlem2  21830  mplcoe1  21965  mplcoe5  21968  evlslem1  22010  mdetunilem7  22526  mdetunilem8  22527  mdetunilem9  22528  mdetuni0  22529  mdetmul  22531  cayhamlem3  22795  ppttop  22915  epttop  22917  cnhaus  23262  isreg2  23285  cncmp  23300  1stcfb  23353  2ndcomap  23366  1stccnp  23370  cldllycmp  23403  1stckgenlem  23461  txcls  23512  ptcnp  23530  txdis1cn  23543  txlly  23544  txnlly  23545  pthaus  23546  txhaus  23555  txkgen  23560  xkohaus  23561  xkococnlem  23567  xkococn  23568  opnfbas  23750  hausflimi  23888  hausflim  23889  hauspwpwf1  23895  alexsubALT  23959  tgpconncomp  24021  qustgplem  24029  metequiv2  24418  met2ndci  24430  nrmmetd  24482  nlmvscnlem1  24594  reconn  24737  xrge0tsms  24743  mulc1cncf  24818  ipcnlem1  25165  minveclem3  25349  pmltpc  25371  ovolicc2lem5  25442  ovolicc2  25443  uniioombllem6  25509  dyadmbllem  25520  vitalilem3  25531  mbfmullem  25646  itg2split  25670  itg2mono  25674  bddiblnc  25763  dvlip2  25920  lhop1  25939  dvcnvrelem1  25942  dvfsumrlim  25958  ftc1lem6  25968  itgsubst  25976  dgrco  26201  plyexmo  26241  ulmdvlem3  26331  abelthlem2  26362  abelthlem8  26369  mpodvdsmulf1o  27124  dvdsmulf1o  27126  chpchtsum  27150  dchrptlem2  27196  2sqlem5  27353  2sqlem9  27358  2sqb  27363  chpo1ubb  27412  vmadivsumb  27414  selbergb  27480  selberg2b  27483  selberg3lem2  27489  pntrsumbnd  27497  pntrlog2bnd  27515  pntibndlem3  27523  pnt3  27543  noresle  27629  nosupprefixmo  27632  noinfprefixmo  27633  nosupbday  27637  noinfbday  27652  noinfbnd1lem5  27659  addsprop  27912  mulsproplem9  28056  mulsasslem3  28097  expadds  28351  readdscl  28394  tgjustf  28444  hlcgreu  28589  mirreu3  28625  cgraswap  28791  cgracom  28793  cgratr  28794  flatcgra  28795  acopyeu  28805  axsegcon  28898  ax5seglem9  28908  axeuclid  28934  axcontlem10  28944  axcontlem12  28946  wwlksnredwwlkn0  29867  n4cyclfrgr  30261  frgrnbnb  30263  numclwwlk1lem2fo  30328  ablo4  30520  smcnlem  30667  pjhthmo  31272  pjpjpre  31389  lnconi  32003  resf1o  32703  mgcoval  32957  xrge0tsmsd  33032  erlval  33215  derangenlem  35183  pconnconn  35243  connpconn  35247  cvmfolem  35291  cvmliftmolem2  35294  cvmliftmo  35296  cvmliftlem7  35303  cvmlift2lem10  35324  cvmlift3lem8  35338  linecgr  36094  btwnconn1lem8  36107  btwnconn1lem14  36113  btwnconn3  36116  brsegle  36121  segletr  36127  segleantisym  36128  outsideofeq  36143  linethru  36166  finminlem  36331  nn0prpwlem  36335  neibastop2lem  36373  weiunpo  36478  mblfinlem3  37678  ftc1cnnc  37711  isbnd3  37803  cvlcvr1  39357  athgt  39474  4atlem12  39630  paddasslem12  39849  paddasslem13  39850  cdleme0cp  40232  cdleme42keg  40504  cdleme42mgN  40506  trlord  40587  cdlemg6c  40638  cdlemkid4  40952  dihopelvalcpre  41266  dihmeetlem1N  41308  dihglblem5apreN  41309  dihmeetlem4preN  41324  dihmeetlem6  41327  dihmeetlem10N  41334  dihmeetlem11N  41335  dihmeetlem13N  41337  dihjatcclem4  41439  fsuppssind  42605  prjspner1  42638  mzpcl1  42741  mzpcompact2lem  42763  diophin  42784  pell14qrmulcl  42875  pwssplit4  43101  hbtlem2  43136  iunrelexpuztr  43731  stoweidlem57  46074  stoweidlem61  46078  fourierdlem92  46215  euoreqb  47119  prproropf1olem3  47515  prproropf1olem4  47516  fpprwpprb  47750  cycldlenngric  47938  grimgrtri  47959  2zlidl  48250  lmodvsmdi  48389  2arwcat  49611