Theorem simprll 786

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  fcof1  7260  mpo0  7470  fpr3g  8254  fprresex  8279  eroveu  8782  boxriin  8911  fofinf1o  9265  finsschain  9292  suppeqfsuppbi  9315  fsuppunbi  9325  marypha1lem  9369  wemapsolem  9488  wemapso  9489  wemapso2lem  9490  cantnf  9638  iunfictbso  10060  enfin2i  10268  ttukeylem7  10462  fpwwe2lem2  10580  fpwwe2lem8  10586  fpwwe2lem11  10589  fpwwelem  10593  distrlem4pr  10974  mulcmpblnr  11019  prsrlem1  11020  dedekind  11336  divdivdiv  11882  divmuleq  11886  divadddiv  11896  divsubdiv  11897  lediv12a  12075  xmullem  13257  xlemul1a  13281  seqcaopr  14042  leexp2r  14177  hashf1lem1  14458  hashf1lem2  14459  ccatsymb  14586  wrd2ind  14726  cshweqrep  14824  rtrclreclem4  15064  lo1le  15655  summolem2  15719  summo  15720  prodmolem2  15941  prodmo  15942  bezoutlem3  16551  bezoutlem4  16552  qredeu  16668  pcadd  16901  prmreclem2  16929  vdwlem9  17001  vdwlem10  17002  ramub1lem2  17039  ramub1  17040  prmgaplem7  17069  cofucl  17897  initoeu2  18025  setcmon  18096  poslubmo  18417  posglbmo  18418  rabsubmgmd  18714  issubmd  18816  grprcan  18991  isnsg3  19177  ghmpreima  19254  gaorber  19324  psgneu  19522  odcau  19620  lsmsubm  19669  lsmmod  19691  ablfaclem3  20105  rngpropd  20196  ringpropd  20310  lmodvsmmulgdi  20937  lmodprop2d  20964  lss1d  21003  lindff1  21845  islindf4  21863  assamulgscmlem2  21925  mplcoe1  22063  mplcoe5  22066  evlslem1  22108  mdetunilem7  22651  mdetunilem8  22652  mdetunilem9  22653  mdetuni0  22654  mdetmul  22656  cayhamlem3  22920  ppttop  23040  epttop  23042  cnhaus  23387  isreg2  23410  cncmp  23425  1stcfb  23478  2ndcomap  23491  1stccnp  23495  cldllycmp  23528  1stckgenlem  23586  txcls  23637  ptcnp  23655  txdis1cn  23668  txlly  23669  txnlly  23670  pthaus  23671  txhaus  23680  txkgen  23685  xkohaus  23686  xkococnlem  23692  xkococn  23693  opnfbas  23875  hausflimi  24013  hausflim  24014  hauspwpwf1  24020  alexsubALT  24084  tgpconncomp  24146  qustgplem  24154  metequiv2  24543  met2ndci  24555  nrmmetd  24607  nlmvscnlem1  24719  reconn  24862  xrge0tsms  24868  mulc1cncf  24940  ipcnlem1  25280  minveclem3  25464  pmltpc  25485  ovolicc2lem5  25556  ovolicc2  25557  uniioombllem6  25623  dyadmbllem  25634  vitalilem3  25645  mbfmullem  25760  itg2split  25784  itg2mono  25788  bddiblnc  25877  dvlip2  26030  lhop1  26049  dvcnvrelem1  26052  dvfsumrlim  26066  ftc1lem6  26076  itgsubst  26084  dgrco  26308  plyexmo  26347  ulmdvlem3  26435  abelthlem2  26465  abelthlem8  26472  mpodvdsmulf1o  27228  dvdsmulf1o  27230  chpchtsum  27253  dchrptlem2  27299  2sqlem5  27456  2sqlem9  27461  2sqb  27466  chpo1ubb  27515  vmadivsumb  27517  selbergb  27583  selberg2b  27586  selberg3lem2  27592  pntrsumbnd  27600  pntrlog2bnd  27618  pntibndlem3  27626  pnt3  27646  noresle  27731  nosupprefixmo  27734  noinfprefixmo  27735  nosupbday  27739  noinfbday  27754  noinfbnd1lem5  27761  addsprop  28039  mulsproplem9  28187  mulsasslem3  28228  expadds  28498  bdayfinbndlem1  28530  readdscl  28562  tgjustf  28612  hlcgreu  28757  mirreu3  28793  cgraswap  28959  cgracom  28961  cgratr  28962  flatcgra  28963  acopyeu  28973  axsegcon  29067  ax5seglem9  29077  axeuclid  29103  axcontlem10  29113  axcontlem12  29115  wwlksnredwwlkn0  30035  n4cyclfrgr  30432  frgrnbnb  30434  numclwwlk1lem2fo  30499  ablo4  30692  smcnlem  30839  pjhthmo  31444  pjpjpre  31561  lnconi  32175  resf1o  32875  mgcoval  33118  xrge0tsmsd  33207  erlval  33393  derangenlem  35469  pconnconn  35529  connpconn  35533  cvmfolem  35577  cvmliftmolem2  35580  cvmliftmo  35582  cvmliftlem7  35589  cvmlift2lem10  35610  cvmlift3lem8  35624  linecgr  36379  btwnconn1lem8  36392  btwnconn1lem14  36398  btwnconn3  36401  brsegle  36406  segletr  36412  segleantisym  36413  outsideofeq  36428  linethru  36451  finminlem  36626  nn0prpwlem  36630  neibastop2lem  36668  weiunpo  36773  mblfinlem3  38106  ftc1cnnc  38139  isbnd3  38231  cvlcvr1  39911  athgt  40028  4atlem12  40184  paddasslem12  40403  paddasslem13  40404  cdleme0cp  40786  cdleme42keg  41058  cdleme42mgN  41060  trlord  41141  cdlemg6c  41192  cdlemkid4  41506  dihopelvalcpre  41820  dihmeetlem1N  41862  dihglblem5apreN  41863  dihmeetlem4preN  41878  dihmeetlem6  41881  dihmeetlem10N  41888  dihmeetlem11N  41889  dihmeetlem13N  41891  dihjatcclem4  41993  fsuppssind  43123  prjspner1  43156  mzpcl1  43258  mzpcompact2lem  43280  diophin  43301  pell14qrmulcl  43388  pwssplit4  43614  hbtlem2  43649  iunrelexpuztr  44243  stoweidlem57  46579  stoweidlem61  46583  fourierdlem92  46720  euoreqb  47651  prproropf1olem3  48059  prproropf1olem4  48060  fpprwpprb  48310  cycldlenngric  48498  grimgrtri  48519  2zlidl  48810  lmodvsmdi  48949  2arwcat  50169