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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  fcof1  7097  mpo0  7296  fpr3g  8026  wfrlem17  8071  eroveu  8494  boxriin  8621  undom  8733  fofinf1o  8951  finsschain  8983  suppeqfsuppbi  8999  fsuppunbi  9006  marypha1lem  9049  wemapsolem  9166  wemapso  9167  wemapso2lem  9168  cantnf  9308  iunfictbso  9728  enfin2i  9935  ttukeylem7  10129  fpwwe2lem2  10246  fpwwe2lem8  10252  fpwwe2lem11  10255  fpwwelem  10259  distrlem4pr  10640  mulcmpblnr  10685  prsrlem1  10686  dedekind  10995  divdivdiv  11533  divmuleq  11537  divadddiv  11547  divsubdiv  11548  lediv12a  11725  xmullem  12854  xlemul1a  12878  seqcaopr  13613  leexp2r  13744  hashf1lem1  14020  hashf1lem1OLD  14021  hashf1lem2  14022  ccatsymb  14139  wrd2ind  14288  cshweqrep  14386  rtrclreclem4  14624  lo1le  15215  summolem2  15280  summo  15281  prodmolem2  15497  prodmo  15498  bezoutlem3  16101  bezoutlem4  16102  qredeu  16215  pcadd  16442  prmreclem2  16470  vdwlem9  16542  vdwlem10  16543  ramub1lem2  16580  ramub1  16581  prmgaplem7  16610  cofucl  17394  initoeu2  17522  setcmon  17593  poslubmo  17917  posglbmo  17918  issubmd  18233  grprcan  18401  isnsg3  18576  ghmpreima  18644  gaorber  18702  psgneu  18898  odcau  18993  lsmsubm  19042  lsmmod  19065  ablfaclem3  19474  ringpropd  19600  lmodvsmmulgdi  19934  lmodprop2d  19961  lss1d  20000  lindff1  20782  islindf4  20800  assamulgscmlem2  20860  mplcoe1  20994  mplcoe5  20997  evlslem1  21042  mdetunilem7  21515  mdetunilem8  21516  mdetunilem9  21517  mdetuni0  21518  mdetmul  21520  cayhamlem3  21784  ppttop  21904  epttop  21906  cnhaus  22251  isreg2  22274  cncmp  22289  1stcfb  22342  2ndcomap  22355  1stccnp  22359  cldllycmp  22392  1stckgenlem  22450  txcls  22501  ptcnp  22519  txdis1cn  22532  txlly  22533  txnlly  22534  pthaus  22535  txhaus  22544  txkgen  22549  xkohaus  22550  xkococnlem  22556  xkococn  22557  opnfbas  22739  hausflimi  22877  hausflim  22878  hauspwpwf1  22884  alexsubALT  22948  tgpconncomp  23010  qustgplem  23018  metequiv2  23408  met2ndci  23420  nrmmetd  23472  nlmvscnlem1  23584  reconn  23725  xrge0tsms  23731  mulc1cncf  23802  ipcnlem1  24142  minveclem3  24326  pmltpc  24347  ovolicc2lem5  24418  ovolicc2  24419  uniioombllem6  24485  dyadmbllem  24496  vitalilem3  24507  mbfmullem  24623  itg2split  24647  itg2mono  24651  bddiblnc  24739  dvlip2  24892  lhop1  24911  dvcnvrelem1  24914  dvfsumrlim  24928  ftc1lem6  24938  itgsubst  24946  dgrco  25169  plyexmo  25206  ulmdvlem3  25294  abelthlem2  25324  abelthlem8  25331  dvdsmulf1o  26076  chpchtsum  26100  dchrptlem2  26146  2sqlem5  26303  2sqlem9  26308  2sqb  26313  chpo1ubb  26362  vmadivsumb  26364  selbergb  26430  selberg2b  26433  selberg3lem2  26439  pntrsumbnd  26447  pntrlog2bnd  26465  pntibndlem3  26473  pnt3  26493  tgjustf  26564  hlcgreu  26709  mirreu3  26745  cgraswap  26911  cgracom  26913  cgratr  26914  flatcgra  26915  acopyeu  26925  axsegcon  27018  ax5seglem9  27028  axeuclid  27054  axcontlem10  27064  axcontlem12  27066  wwlksnredwwlkn0  27980  n4cyclfrgr  28374  frgrnbnb  28376  numclwwlk1lem2fo  28441  ablo4  28631  smcnlem  28778  pjhthmo  29383  pjpjpre  29500  lnconi  30114  resf1o  30785  mgcoval  30983  xrge0tsmsd  31036  derangenlem  32846  pconnconn  32906  connpconn  32910  cvmfolem  32954  cvmliftmolem2  32957  cvmliftmo  32959  cvmliftlem7  32966  cvmlift2lem10  32987  cvmlift3lem8  33001  noresle  33637  nosupprefixmo  33640  noinfprefixmo  33641  nosupbday  33645  noinfbday  33660  noinfbnd1lem5  33667  linecgr  34120  btwnconn1lem8  34133  btwnconn1lem14  34139  btwnconn3  34142  brsegle  34147  segletr  34153  segleantisym  34154  outsideofeq  34169  linethru  34192  finminlem  34244  nn0prpwlem  34248  neibastop2lem  34286  mblfinlem3  35553  ftc1cnnc  35586  isbnd3  35679  cvlcvr1  37090  athgt  37207  4atlem12  37363  paddasslem12  37582  paddasslem13  37583  cdleme0cp  37965  cdleme42keg  38237  cdleme42mgN  38239  trlord  38320  cdlemg6c  38371  cdlemkid4  38685  dihopelvalcpre  38999  dihmeetlem1N  39041  dihglblem5apreN  39042  dihmeetlem4preN  39057  dihmeetlem6  39060  dihmeetlem10N  39067  dihmeetlem11N  39068  dihmeetlem13N  39070  dihjatcclem4  39172  fsuppssind  39992  prjspner1  40171  mzpcl1  40254  mzpcompact2lem  40276  diophin  40297  pell14qrmulcl  40388  pwssplit4  40617  hbtlem2  40652  iunrelexpuztr  41004  stoweidlem57  43273  stoweidlem61  43277  fourierdlem92  43414  euoreqb  44273  prproropf1olem3  44630  prproropf1olem4  44631  fpprwpprb  44865  rabsubmgmd  45018  2zlidl  45165  lmodvsmdi  45391