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 729	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  7235  mpo0  7445  fpr3g  8229  fprresex  8254  eroveu  8753  boxriin  8882  fofinf1o  9236  finsschain  9263  suppeqfsuppbi  9286  fsuppunbi  9296  marypha1lem  9340  wemapsolem  9459  wemapso  9460  wemapso2lem  9461  cantnf  9606  iunfictbso  10028  enfin2i  10235  ttukeylem7  10429  fpwwe2lem2  10547  fpwwe2lem8  10553  fpwwe2lem11  10556  fpwwelem  10560  distrlem4pr  10941  mulcmpblnr  10986  prsrlem1  10987  dedekind  11300  divdivdiv  11846  divmuleq  11850  divadddiv  11860  divsubdiv  11861  lediv12a  12039  xmullem  13183  xlemul1a  13207  seqcaopr  13966  leexp2r  14101  hashf1lem1  14382  hashf1lem2  14383  ccatsymb  14510  wrd2ind  14650  cshweqrep  14748  rtrclreclem4  14988  lo1le  15579  summolem2  15643  summo  15644  prodmolem2  15862  prodmo  15863  bezoutlem3  16472  bezoutlem4  16473  qredeu  16589  pcadd  16821  prmreclem2  16849  vdwlem9  16921  vdwlem10  16922  ramub1lem2  16959  ramub1  16960  prmgaplem7  16989  cofucl  17816  initoeu2  17944  setcmon  18015  poslubmo  18336  posglbmo  18337  rabsubmgmd  18633  issubmd  18735  grprcan  18907  isnsg3  19093  ghmpreima  19171  gaorber  19241  psgneu  19439  odcau  19537  lsmsubm  19586  lsmmod  19608  ablfaclem3  20022  rngpropd  20113  ringpropd  20227  lmodvsmmulgdi  20852  lmodprop2d  20879  lss1d  20918  lindff1  21779  islindf4  21797  assamulgscmlem2  21860  mplcoe1  21996  mplcoe5  21999  evlslem1  22041  mdetunilem7  22566  mdetunilem8  22567  mdetunilem9  22568  mdetuni0  22569  mdetmul  22571  cayhamlem3  22835  ppttop  22955  epttop  22957  cnhaus  23302  isreg2  23325  cncmp  23340  1stcfb  23393  2ndcomap  23406  1stccnp  23410  cldllycmp  23443  1stckgenlem  23501  txcls  23552  ptcnp  23570  txdis1cn  23583  txlly  23584  txnlly  23585  pthaus  23586  txhaus  23595  txkgen  23600  xkohaus  23601  xkococnlem  23607  xkococn  23608  opnfbas  23790  hausflimi  23928  hausflim  23929  hauspwpwf1  23935  alexsubALT  23999  tgpconncomp  24061  qustgplem  24069  metequiv2  24458  met2ndci  24470  nrmmetd  24522  nlmvscnlem1  24634  reconn  24777  xrge0tsms  24783  mulc1cncf  24858  ipcnlem1  25205  minveclem3  25389  pmltpc  25411  ovolicc2lem5  25482  ovolicc2  25483  uniioombllem6  25549  dyadmbllem  25560  vitalilem3  25571  mbfmullem  25686  itg2split  25710  itg2mono  25714  bddiblnc  25803  dvlip2  25960  lhop1  25979  dvcnvrelem1  25982  dvfsumrlim  25998  ftc1lem6  26008  itgsubst  26016  dgrco  26241  plyexmo  26281  ulmdvlem3  26371  abelthlem2  26402  abelthlem8  26409  mpodvdsmulf1o  27164  dvdsmulf1o  27166  chpchtsum  27190  dchrptlem2  27236  2sqlem5  27393  2sqlem9  27398  2sqb  27403  chpo1ubb  27452  vmadivsumb  27454  selbergb  27520  selberg2b  27523  selberg3lem2  27529  pntrsumbnd  27537  pntrlog2bnd  27555  pntibndlem3  27563  pnt3  27583  noresle  27669  nosupprefixmo  27672  noinfprefixmo  27673  nosupbday  27677  noinfbday  27692  noinfbnd1lem5  27699  addsprop  27958  mulsproplem9  28106  mulsasslem3  28147  expadds  28414  bdayfinbndlem1  28446  readdscl  28478  tgjustf  28528  hlcgreu  28673  mirreu3  28709  cgraswap  28875  cgracom  28877  cgratr  28878  flatcgra  28879  acopyeu  28889  axsegcon  28983  ax5seglem9  28993  axeuclid  29019  axcontlem10  29029  axcontlem12  29031  wwlksnredwwlkn0  29952  n4cyclfrgr  30349  frgrnbnb  30351  numclwwlk1lem2fo  30416  ablo4  30608  smcnlem  30755  pjhthmo  31360  pjpjpre  31477  lnconi  32091  resf1o  32790  mgcoval  33049  xrge0tsmsd  33136  erlval  33321  derangenlem  35346  pconnconn  35406  connpconn  35410  cvmfolem  35454  cvmliftmolem2  35457  cvmliftmo  35459  cvmliftlem7  35466  cvmlift2lem10  35487  cvmlift3lem8  35501  linecgr  36256  btwnconn1lem8  36269  btwnconn1lem14  36275  btwnconn3  36278  brsegle  36283  segletr  36289  segleantisym  36290  outsideofeq  36305  linethru  36328  finminlem  36493  nn0prpwlem  36497  neibastop2lem  36535  weiunpo  36640  mblfinlem3  37831  ftc1cnnc  37864  isbnd3  37956  cvlcvr1  39636  athgt  39753  4atlem12  39909  paddasslem12  40128  paddasslem13  40129  cdleme0cp  40511  cdleme42keg  40783  cdleme42mgN  40785  trlord  40866  cdlemg6c  40917  cdlemkid4  41231  dihopelvalcpre  41545  dihmeetlem1N  41587  dihglblem5apreN  41588  dihmeetlem4preN  41603  dihmeetlem6  41606  dihmeetlem10N  41613  dihmeetlem11N  41614  dihmeetlem13N  41616  dihjatcclem4  41718  fsuppssind  42872  prjspner1  42905  mzpcl1  43007  mzpcompact2lem  43029  diophin  43050  pell14qrmulcl  43141  pwssplit4  43367  hbtlem2  43402  iunrelexpuztr  43996  stoweidlem57  46337  stoweidlem61  46341  fourierdlem92  46478  euoreqb  47391  prproropf1olem3  47787  prproropf1olem4  47788  fpprwpprb  48022  cycldlenngric  48210  grimgrtri  48231  2zlidl  48522  lmodvsmdi  48661  2arwcat  49881