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  7291  mpo0  7501  fpr3g  8287  fprresex  8312  eroveu  8815  boxriin  8950  fofinf1o  9302  finsschain  9329  suppeqfsuppbi  9352  fsuppunbi  9362  marypha1lem  9406  wemapsolem  9525  wemapso  9526  wemapso2lem  9527  cantnf  9675  iunfictbso  10120  enfin2i  10326  ttukeylem7  10520  fpwwe2lem2  10644  fpwwe2lem8  10650  fpwwe2lem11  10653  fpwwelem  10657  distrlem4pr  11038  mulcmpblnr  11083  prsrlem1  11084  dedekind  11400  divdivdiv  11943  divmuleq  11947  divadddiv  11957  divsubdiv  11958  lediv12a  12135  xmullem  13318  xlemul1a  13342  seqcaopr  14105  leexp2r  14240  hashf1lem1  14522  hashf1lem2  14523  ccatsymb  14650  wrd2ind  14794  cshweqrep  14894  rtrclreclem4  15136  lo1le  15741  summolem2  15804  summo  15805  prodmolem2  16026  prodmo  16027  bezoutlem3  16635  bezoutlem4  16636  qredeu  16752  pcadd  16985  prmreclem2  17013  vdwlem9  17085  vdwlem10  17086  ramub1lem2  17123  ramub1  17124  prmgaplem7  17153  cofucl  17981  initoeu2  18109  setcmon  18180  poslubmo  18501  posglbmo  18502  rabsubmgmd  18810  issubmd  18918  grprcan  19101  isnsg3  19287  ghmpreima  19369  gaorber  19439  psgneu  19637  odcau  19735  lsmsubm  19784  lsmmod  19806  ablfaclem3  20220  rngpropd  20313  ringpropd  20434  lmodvsmmulgdi  21085  lmodprop2d  21112  lss1d  21151  lindff1  22037  islindf4  22055  assamulgscmlem2  22119  mplcoe1  22257  mplcoe5  22260  evlslem1  22302  mdetunilem7  22844  mdetunilem8  22845  mdetunilem9  22846  mdetuni0  22847  mdetmul  22849  cayhamlem3  23116  ppttop  23236  epttop  23238  cnhaus  23583  isreg2  23606  cncmp  23621  1stcfb  23674  2ndcomap  23688  1stccnp  23692  cldllycmp  23725  1stckgenlem  23783  txcls  23834  ptcnp  23852  txdis1cn  23865  txlly  23866  txnlly  23867  pthaus  23868  txhaus  23877  txkgen  23882  xkohaus  23883  xkococnlem  23889  xkococn  23890  opnfbas  24072  hausflimi  24210  hausflim  24211  hauspwpwf1  24217  alexsubALT  24281  tgpconncomp  24343  qustgplem  24351  metequiv2  24740  met2ndci  24752  nrmmetd  24804  nlmvscnlem1  24916  reconn  25059  xrge0tsms  25065  mulc1cncf  25137  ipcnlem1  25477  minveclem3  25661  pmltpc  25682  ovolicc2lem5  25753  ovolicc2  25754  uniioombllem6  25820  dyadmbllem  25831  vitalilem3  25842  mbfmullem  25957  itg2split  25981  itg2mono  25985  bddiblnc  26074  dvlip2  26227  lhop1  26246  dvcnvrelem1  26249  dvfsumrlim  26263  ftc1lem6  26273  itgsubst  26281  dgrco  26505  plyexmo  26547  ulmdvlem3  26638  abelthlem2  26668  abelthlem8  26675  mpodvdsmulf1o  27431  dvdsmulf1o  27433  chpchtsum  27456  dchrptlem2  27502  2sqlem5  27659  2sqlem9  27664  2sqb  27669  chpo1ubb  27718  vmadivsumb  27720  selbergb  27786  selberg2b  27789  selberg3lem2  27795  pntrsumbnd  27803  pntrlog2bnd  27821  pntibndlem3  27829  pnt3  27849  noresle  27934  nosupprefixmo  27937  noinfprefixmo  27938  nosupbday  27942  noinfbday  27957  noinfbnd1lem5  27964  addsprop  28242  mulsproplem9  28390  mulsasslem3  28431  expadds  28701  bdayfinbndlem1  28733  readdscl  28765  tgjustf  28815  hlcgreu  28964  mirreu3  29006  cgraswap  29207  cgracom  29209  cgratr  29210  flatcgra  29212  acopyeu  29222  brprlng  29296  axsegcon  29385  ax5seglem9  29395  axeuclid  29421  axcontlem10  29431  axcontlem12  29433  wwlksnredwwlkn0  30365  n4cyclfrgr  30772  frgrnbnb  30774  numclwwlk1lem2fo  30839  ablo4  31032  smcnlem  31179  pjhthmo  31784  pjpjpre  31901  lnconi  32515  resf1o  33203  mgcoval  33428  xrge0tsmsd  33515  erlval  33700  derangenlem  35752  pconnconn  35812  connpconn  35816  cvmfolem  35860  cvmliftmolem2  35863  cvmliftmo  35865  cvmliftlem7  35872  cvmlift2lem10  35893  cvmlift3lem8  35907  linecgr  36663  btwnconn1lem8  36676  btwnconn1lem14  36682  btwnconn3  36685  brsegle  36690  segletr  36696  segleantisym  36697  outsideofeq  36712  linethru  36735  nadddilem1  36802  finminlem  36939  nn0prpwlem  36943  neibastop2lem  36981  weiunpo  37086  mblfinlem3  38410  ftc1cnnc  38443  isbnd3  38536  cvlcvr1  40214  athgt  40331  4atlem12  40487  paddasslem12  40706  paddasslem13  40707  cdleme0cp  41089  cdleme42keg  41361  cdleme42mgN  41363  trlord  41444  cdlemg6c  41495  cdlemkid4  41809  dihopelvalcpre  42123  dihmeetlem1N  42165  dihglblem5apreN  42166  dihmeetlem4preN  42181  dihmeetlem6  42184  dihmeetlem10N  42191  dihmeetlem11N  42192  dihmeetlem13N  42194  dihjatcclem4  42296  fsuppssind  43441  prjspner1  43474  mzpcl1  43576  mzpcompact2lem  43598  diophin  43619  pell14qrmulcl  43706  pwssplit4  43932  hbtlem2  43967  iunrelexpuztr  44561  stoweidlem57  46887  stoweidlem61  46891  fourierdlem92  47028  euoreqb  47999  prproropf1olem3  48407  prproropf1olem4  48408  fpprwpprb  48658  cycldlenngric  48846  grimgrtri  48867  2zlidl  49157  lmodvsmdi  49311  2arwcat  50528