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  7242  mpo0  7452  fpr3g  8235  fprresex  8260  eroveu  8759  boxriin  8888  fofinf1o  9242  finsschain  9269  suppeqfsuppbi  9292  fsuppunbi  9302  marypha1lem  9346  wemapsolem  9465  wemapso  9466  wemapso2lem  9467  cantnf  9614  iunfictbso  10036  enfin2i  10243  ttukeylem7  10437  fpwwe2lem2  10555  fpwwe2lem8  10561  fpwwe2lem11  10564  fpwwelem  10568  distrlem4pr  10949  mulcmpblnr  10994  prsrlem1  10995  dedekind  11309  divdivdiv  11856  divmuleq  11860  divadddiv  11870  divsubdiv  11871  lediv12a  12049  xmullem  13216  xlemul1a  13240  seqcaopr  14001  leexp2r  14136  hashf1lem1  14417  hashf1lem2  14418  ccatsymb  14545  wrd2ind  14685  cshweqrep  14783  rtrclreclem4  15023  lo1le  15614  summolem2  15678  summo  15679  prodmolem2  15900  prodmo  15901  bezoutlem3  16510  bezoutlem4  16511  qredeu  16627  pcadd  16860  prmreclem2  16888  vdwlem9  16960  vdwlem10  16961  ramub1lem2  16998  ramub1  16999  prmgaplem7  17028  cofucl  17855  initoeu2  17983  setcmon  18054  poslubmo  18375  posglbmo  18376  rabsubmgmd  18672  issubmd  18774  grprcan  18949  isnsg3  19135  ghmpreima  19213  gaorber  19283  psgneu  19481  odcau  19579  lsmsubm  19628  lsmmod  19650  ablfaclem3  20064  rngpropd  20155  ringpropd  20269  lmodvsmmulgdi  20892  lmodprop2d  20919  lss1d  20958  lindff1  21800  islindf4  21818  assamulgscmlem2  21880  mplcoe1  22015  mplcoe5  22018  evlslem1  22060  mdetunilem7  22583  mdetunilem8  22584  mdetunilem9  22585  mdetuni0  22586  mdetmul  22588  cayhamlem3  22852  ppttop  22972  epttop  22974  cnhaus  23319  isreg2  23342  cncmp  23357  1stcfb  23410  2ndcomap  23423  1stccnp  23427  cldllycmp  23460  1stckgenlem  23518  txcls  23569  ptcnp  23587  txdis1cn  23600  txlly  23601  txnlly  23602  pthaus  23603  txhaus  23612  txkgen  23617  xkohaus  23618  xkococnlem  23624  xkococn  23625  opnfbas  23807  hausflimi  23945  hausflim  23946  hauspwpwf1  23952  alexsubALT  24016  tgpconncomp  24078  qustgplem  24086  metequiv2  24475  met2ndci  24487  nrmmetd  24539  nlmvscnlem1  24651  reconn  24794  xrge0tsms  24800  mulc1cncf  24872  ipcnlem1  25212  minveclem3  25396  pmltpc  25417  ovolicc2lem5  25488  ovolicc2  25489  uniioombllem6  25555  dyadmbllem  25566  vitalilem3  25577  mbfmullem  25692  itg2split  25716  itg2mono  25720  bddiblnc  25809  dvlip2  25962  lhop1  25981  dvcnvrelem1  25984  dvfsumrlim  25998  ftc1lem6  26008  itgsubst  26016  dgrco  26240  plyexmo  26279  ulmdvlem3  26367  abelthlem2  26397  abelthlem8  26404  mpodvdsmulf1o  27157  dvdsmulf1o  27159  chpchtsum  27182  dchrptlem2  27228  2sqlem5  27385  2sqlem9  27390  2sqb  27395  chpo1ubb  27444  vmadivsumb  27446  selbergb  27512  selberg2b  27515  selberg3lem2  27521  pntrsumbnd  27529  pntrlog2bnd  27547  pntibndlem3  27555  pnt3  27575  noresle  27661  nosupprefixmo  27664  noinfprefixmo  27665  nosupbday  27669  noinfbday  27684  noinfbnd1lem5  27691  addsprop  27968  mulsproplem9  28116  mulsasslem3  28157  expadds  28427  bdayfinbndlem1  28459  readdscl  28491  tgjustf  28541  hlcgreu  28686  mirreu3  28722  cgraswap  28888  cgracom  28890  cgratr  28891  flatcgra  28892  acopyeu  28902  axsegcon  28996  ax5seglem9  29006  axeuclid  29032  axcontlem10  29042  axcontlem12  29044  wwlksnredwwlkn0  29964  n4cyclfrgr  30361  frgrnbnb  30363  numclwwlk1lem2fo  30428  ablo4  30621  smcnlem  30768  pjhthmo  31373  pjpjpre  31490  lnconi  32104  resf1o  32803  mgcoval  33046  xrge0tsmsd  33134  erlval  33319  derangenlem  35353  pconnconn  35413  connpconn  35417  cvmfolem  35461  cvmliftmolem2  35464  cvmliftmo  35466  cvmliftlem7  35473  cvmlift2lem10  35494  cvmlift3lem8  35508  linecgr  36263  btwnconn1lem8  36276  btwnconn1lem14  36282  btwnconn3  36285  brsegle  36290  segletr  36296  segleantisym  36297  outsideofeq  36312  linethru  36335  finminlem  36500  nn0prpwlem  36504  neibastop2lem  36542  weiunpo  36647  mblfinlem3  37980  ftc1cnnc  38013  isbnd3  38105  cvlcvr1  39785  athgt  39902  4atlem12  40058  paddasslem12  40277  paddasslem13  40278  cdleme0cp  40660  cdleme42keg  40932  cdleme42mgN  40934  trlord  41015  cdlemg6c  41066  cdlemkid4  41380  dihopelvalcpre  41694  dihmeetlem1N  41736  dihglblem5apreN  41737  dihmeetlem4preN  41752  dihmeetlem6  41755  dihmeetlem10N  41762  dihmeetlem11N  41763  dihmeetlem13N  41765  dihjatcclem4  41867  fsuppssind  43026  prjspner1  43059  mzpcl1  43161  mzpcompact2lem  43183  diophin  43204  pell14qrmulcl  43291  pwssplit4  43517  hbtlem2  43552  iunrelexpuztr  44146  stoweidlem57  46485  stoweidlem61  46489  fourierdlem92  46626  euoreqb  47551  prproropf1olem3  47959  prproropf1olem4  47960  fpprwpprb  48210  cycldlenngric  48398  grimgrtri  48419  2zlidl  48710  lmodvsmdi  48849  2arwcat  50069