Theorem simprll 790

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  fcof1  7285  mpo0  7495  fpr3g  8281  fprresex  8306  eroveu  8809  boxriin  8937  fofinf1o  9288  finsschain  9315  suppeqfsuppbi  9338  fsuppunbi  9348  marypha1lem  9392  wemapsolem  9511  wemapso  9512  wemapso2lem  9513  cantnf  9661  iunfictbso  10097  enfin2i  10304  ttukeylem7  10498  fpwwe2lem2  10616  fpwwe2lem8  10622  fpwwe2lem11  10625  fpwwelem  10629  distrlem4pr  11010  mulcmpblnr  11055  prsrlem1  11056  dedekind  11372  divdivdiv  11915  divmuleq  11919  divadddiv  11929  divsubdiv  11930  lediv12a  12107  xmullem  13289  xlemul1a  13313  seqcaopr  14075  leexp2r  14210  hashf1lem1  14492  hashf1lem2  14493  ccatsymb  14620  wrd2ind  14760  cshweqrep  14858  rtrclreclem4  15098  lo1le  15703  summolem2  15767  summo  15768  prodmolem2  15989  prodmo  15990  bezoutlem3  16598  bezoutlem4  16599  qredeu  16715  pcadd  16948  prmreclem2  16976  vdwlem9  17048  vdwlem10  17049  ramub1lem2  17086  ramub1  17087  prmgaplem7  17116  cofucl  17944  initoeu2  18072  setcmon  18143  poslubmo  18464  posglbmo  18465  rabsubmgmd  18761  issubmd  18863  grprcan  19039  isnsg3  19225  ghmpreima  19307  gaorber  19377  psgneu  19575  odcau  19673  lsmsubm  19722  lsmmod  19744  ablfaclem3  20158  rngpropd  20251  ringpropd  20370  lmodvsmmulgdi  20997  lmodprop2d  21024  lss1d  21063  lindff1  21949  islindf4  21967  assamulgscmlem2  22029  mplcoe1  22167  mplcoe5  22170  evlslem1  22212  mdetunilem7  22754  mdetunilem8  22755  mdetunilem9  22756  mdetuni0  22757  mdetmul  22759  cayhamlem3  23023  ppttop  23143  epttop  23145  cnhaus  23490  isreg2  23513  cncmp  23528  1stcfb  23581  2ndcomap  23594  1stccnp  23598  cldllycmp  23631  1stckgenlem  23689  txcls  23740  ptcnp  23758  txdis1cn  23771  txlly  23772  txnlly  23773  pthaus  23774  txhaus  23783  txkgen  23788  xkohaus  23789  xkococnlem  23795  xkococn  23796  opnfbas  23978  hausflimi  24116  hausflim  24117  hauspwpwf1  24123  alexsubALT  24187  tgpconncomp  24249  qustgplem  24257  metequiv2  24646  met2ndci  24658  nrmmetd  24710  nlmvscnlem1  24822  reconn  24965  xrge0tsms  24971  mulc1cncf  25043  ipcnlem1  25383  minveclem3  25567  pmltpc  25588  ovolicc2lem5  25659  ovolicc2  25660  uniioombllem6  25726  dyadmbllem  25737  vitalilem3  25748  mbfmullem  25863  itg2split  25887  itg2mono  25891  bddiblnc  25980  dvlip2  26133  lhop1  26152  dvcnvrelem1  26155  dvfsumrlim  26169  ftc1lem6  26179  itgsubst  26187  dgrco  26411  plyexmo  26453  ulmdvlem3  26541  abelthlem2  26571  abelthlem8  26578  mpodvdsmulf1o  27334  dvdsmulf1o  27336  chpchtsum  27359  dchrptlem2  27405  2sqlem5  27562  2sqlem9  27567  2sqb  27572  chpo1ubb  27621  vmadivsumb  27623  selbergb  27689  selberg2b  27692  selberg3lem2  27698  pntrsumbnd  27706  pntrlog2bnd  27724  pntibndlem3  27732  pnt3  27752  noresle  27837  nosupprefixmo  27840  noinfprefixmo  27841  nosupbday  27845  noinfbday  27860  noinfbnd1lem5  27867  addsprop  28145  mulsproplem9  28293  mulsasslem3  28334  expadds  28604  bdayfinbndlem1  28636  readdscl  28668  tgjustf  28718  hlcgreu  28866  mirreu3  28907  cgraswap  29104  cgracom  29106  cgratr  29107  flatcgra  29108  acopyeu  29118  brprlng  29161  axsegcon  29243  ax5seglem9  29253  axeuclid  29279  axcontlem10  29289  axcontlem12  29291  wwlksnredwwlkn0  30211  n4cyclfrgr  30608  frgrnbnb  30610  numclwwlk1lem2fo  30675  ablo4  30868  smcnlem  31015  pjhthmo  31620  pjpjpre  31737  lnconi  32351  resf1o  33041  mgcoval  33272  xrge0tsmsd  33359  erlval  33544  derangenlem  35629  pconnconn  35689  connpconn  35693  cvmfolem  35737  cvmliftmolem2  35740  cvmliftmo  35742  cvmliftlem7  35749  cvmlift2lem10  35770  cvmlift3lem8  35784  linecgr  36539  btwnconn1lem8  36552  btwnconn1lem14  36558  btwnconn3  36561  brsegle  36566  segletr  36572  segleantisym  36573  outsideofeq  36588  linethru  36611  finminlem  36795  nn0prpwlem  36799  neibastop2lem  36837  weiunpo  36942  mblfinlem3  38276  ftc1cnnc  38309  isbnd3  38401  cvlcvr1  40081  athgt  40198  4atlem12  40354  paddasslem12  40573  paddasslem13  40574  cdleme0cp  40956  cdleme42keg  41228  cdleme42mgN  41230  trlord  41311  cdlemg6c  41362  cdlemkid4  41676  dihopelvalcpre  41990  dihmeetlem1N  42032  dihglblem5apreN  42033  dihmeetlem4preN  42048  dihmeetlem6  42051  dihmeetlem10N  42058  dihmeetlem11N  42059  dihmeetlem13N  42061  dihjatcclem4  42163  fsuppssind  43295  prjspner1  43328  mzpcl1  43430  mzpcompact2lem  43452  diophin  43473  pell14qrmulcl  43560  pwssplit4  43786  hbtlem2  43821  iunrelexpuztr  44415  stoweidlem57  46741  stoweidlem61  46745  fourierdlem92  46882  euoreqb  47813  prproropf1olem3  48221  prproropf1olem4  48222  fpprwpprb  48472  cycldlenngric  48660  grimgrtri  48681  2zlidl  48972  lmodvsmdi  49126  2arwcat  50345