Theorem simprll 791

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fcof1  7295  mpo0  7505  fpr3g  8304  fprresex  8329  eroveu  8834  boxriin  8969  fofinf1o  9322  finsschain  9349  suppeqfsuppbi  9372  fsuppunbi  9382  marypha1lem  9426  wemapsolem  9545  wemapso  9546  wemapso2lem  9547  cantnf  9695  iunfictbso  10194  enfin2i  10400  ttukeylem7  10594  fpwwe2lem2  10718  fpwwe2lem8  10724  fpwwe2lem11  10727  fpwwelem  10731  distrlem4pr  11112  mulcmpblnr  11157  prsrlem1  11158  dedekind  11474  divdivdiv  12019  divmuleq  12023  divadddiv  12033  divsubdiv  12034  lediv12a  12211  xmullem  13395  xlemul1a  13419  seqcaopr  14183  leexp2r  14318  hashf1lem1  14601  hashf1lem2  14602  ccatsymb  14729  wrd2ind  14873  cshweqrep  14973  rtrclreclem4  15215  lo1le  15820  summolem2  15883  summo  15884  prodmolem2  16103  prodmo  16104  bezoutlem3  16715  bezoutlem4  16716  qredeu  16834  pcadd  17068  prmreclem2  17096  vdwlem9  17168  vdwlem10  17169  ramub1lem2  17206  ramub1  17207  prmgaplem7  17236  cofucl  18064  initoeu2  18192  setcmon  18263  poslubmo  18584  posglbmo  18585  rabsubmgmd  18894  issubmd  19002  grprcan  19185  isnsg3  19371  ghmpreima  19453  gaorber  19523  psgneu  19721  odcau  19819  lsmsubm  19868  lsmmod  19890  ablfaclem3  20304  rngpropd  20397  ringpropd  20520  lmodvsmmulgdi  21173  lmodprop2d  21200  lss1d  21239  lindff1  22127  islindf4  22145  assamulgscmlem2  22209  mplcoe1  22347  mplcoe5  22350  evlslem1  22392  mdetunilem7  22934  mdetunilem8  22935  mdetunilem9  22936  mdetuni0  22937  mdetmul  22939  cayhamlem3  23206  ppttop  23326  epttop  23328  cnhaus  23673  isreg2  23696  cncmp  23711  1stcfb  23764  2ndcomap  23778  1stccnp  23782  cldllycmp  23815  1stckgenlem  23873  txcls  23924  ptcnp  23942  txdis1cn  23955  txlly  23956  txnlly  23957  pthaus  23958  txhaus  23967  txkgen  23972  xkohaus  23973  xkococnlem  23979  xkococn  23980  opnfbas  24162  hausflimi  24300  hausflim  24301  hauspwpwf1  24307  alexsubALT  24371  tgpconncomp  24433  qustgplem  24441  metequiv2  24830  met2ndci  24842  nrmmetd  24894  nlmvscnlem1  25006  reconn  25149  xrge0tsms  25155  mulc1cncf  25227  ipcnlem1  25567  minveclem3  25751  pmltpc  25772  ovolicc2lem5  25843  ovolicc2  25844  uniioombllem6  25910  dyadmbllem  25921  vitalilem3  25932  mbfmullem  26047  itg2split  26071  itg2mono  26075  bddiblnc  26163  dvlip2  26316  lhop1  26335  dvcnvrelem1  26338  dvfsumrlim  26352  ftc1lem6  26362  itgsubst  26370  dgrco  26595  plyexmo  26637  ulmdvlem3  26730  abelthlem2  26760  abelthlem8  26767  mpodvdsmulf1o  27522  dvdsmulf1o  27524  chpchtsum  27547  dchrptlem2  27593  2sqlem5  27750  2sqlem9  27755  2sqb  27760  chpo1ubb  27809  vmadivsumb  27811  selbergb  27877  selberg2b  27880  selberg3lem2  27886  pntrsumbnd  27894  pntrlog2bnd  27912  pntibndlem3  27920  pnt3  27940  noresle  28055  nosupprefixmo  28058  noinfprefixmo  28059  nosupbday  28063  noinfbday  28078  noinfbnd1lem5  28085  addsprop  28363  mulsproplem9  28511  mulsasslem3  28552  expadds  28822  bdayfinbndlem1  28854  readdscl  28886  tgjustf  28936  hlcgreu  29085  mirreu3  29127  cgraswap  29328  cgracom  29330  cgratr  29331  flatcgra  29333  acopyeu  29343  brprlng  29417  axsegcon  29506  ax5seglem9  29516  axeuclid  29542  axcontlem10  29552  axcontlem12  29554  wwlksnredwwlkn0  30486  n4cyclfrgr  30893  frgrnbnb  30895  numclwwlk1lem2fo  30960  ablo4  31153  smcnlem  31300  pjhthmo  31905  pjpjpre  32022  lnconi  32636  resf1o  33365  mgcoval  33590  xrge0tsmsd  33677  erlval  33862  derangenlem  36005  pconnconn  36065  connpconn  36069  cvmfolem  36113  cvmliftmolem2  36116  cvmliftmo  36118  cvmliftlem7  36125  cvmlift2lem10  36146  cvmlift3lem8  36160  linecgr  36921  btwnconn1lem8  36934  btwnconn1lem14  36940  btwnconn3  36943  brsegle  36948  segletr  36954  segleantisym  36955  outsideofeq  36970  linethru  36993  nadddilem1  37044  finminlem  37181  nn0prpwlem  37185  neibastop2lem  37223  weiunpo  37328  mblfinlem3  38653  ftc1cnnc  38686  isbnd3  38794  cvlcvr1  40472  athgt  40589  4atlem12  40745  paddasslem12  40964  paddasslem13  40965  cdleme0cp  41347  cdleme42keg  41619  cdleme42mgN  41621  trlord  41702  cdlemg6c  41753  cdlemkid4  42067  dihopelvalcpre  42381  dihmeetlem1N  42423  dihglblem5apreN  42424  dihmeetlem4preN  42439  dihmeetlem6  42442  dihmeetlem10N  42449  dihmeetlem11N  42450  dihmeetlem13N  42452  dihjatcclem4  42554  fsuppssind  43697  mzpcl1  43816  mzpcompact2lem  43838  diophin  43859  pell14qrmulcl  43946  pwssplit4  44167  hbtlem2  44202  iunrelexpuztr  44795  stoweidlem57  47143  stoweidlem61  47147  fourierdlem92  47284  euoreqb  48255  prproropf1olem3  48663  prproropf1olem4  48664  fpprwpprb  48914  cycldlenngric  49102  grimgrtri  49123  2zlidl  49413  lmodvsmdi  49567  2arwcat  50784