Theorem simprll 791

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fcof1  7318  mpo0  7528  fpr3g  8331  fprresex  8356  eroveu  8861  boxriin  8996  fofinf1o  9349  finsschain  9376  suppeqfsuppbi  9398  fsuppunbi  9408  marypha1lem  9452  wemapsolem  9571  wemapso  9572  wemapso2lem  9573  cantnf  9721  iunfictbso  10220  enfin2i  10426  ttukeylem7  10620  fpwwe2lem2  10744  fpwwe2lem8  10750  fpwwe2lem11  10753  fpwwelem  10757  distrlem4pr  11138  mulcmpblnr  11183  prsrlem1  11184  dedekind  11500  divdivdiv  12045  divmuleq  12049  divadddiv  12059  divsubdiv  12060  lediv12a  12237  xmullem  13421  xlemul1a  13445  seqcaopr  14209  leexp2r  14344  hashf1lem1  14627  hashf1lem2  14628  ccatsymb  14755  wrd2ind  14900  cshweqrep  15000  rtrclreclem4  15243  lo1le  15848  summolem2  15911  summo  15912  prodmolem2  16131  prodmo  16132  bezoutlem3  16743  bezoutlem4  16744  qredeu  16862  pcadd  17096  prmreclem2  17124  vdwlem9  17196  vdwlem10  17197  ramub1lem2  17234  ramub1  17235  prmgaplem7  17264  cofucl  18092  initoeu2  18220  setcmon  18291  poslubmo  18612  posglbmo  18613  rabsubmgmd  18922  issubmd  19030  grprcan  19213  isnsg3  19399  ghmpreima  19481  gaorber  19552  psgneu  19750  odcau  19848  lsmsubm  19897  lsmmod  19919  ablfaclem3  20333  rngpropd  20426  ringpropd  20549  lmodvsmmulgdi  21202  lmodprop2d  21229  lss1d  21268  lindff1  22156  islindf4  22174  assamulgscmlem2  22238  mplcoe1  22376  mplcoe5  22379  evlslem1  22421  mdetunilem7  22963  mdetunilem8  22964  mdetunilem9  22965  mdetuni0  22966  mdetmul  22968  cayhamlem3  23235  ppttop  23355  epttop  23357  cnhaus  23702  isreg2  23725  cncmp  23740  1stcfb  23793  2ndcomap  23807  1stccnp  23811  cldllycmp  23844  1stckgenlem  23902  txcls  23953  ptcnp  23971  txdis1cn  23984  txlly  23985  txnlly  23986  pthaus  23987  txhaus  23996  txkgen  24001  xkohaus  24002  xkococnlem  24008  xkococn  24009  opnfbas  24191  hausflimi  24329  hausflim  24330  hauspwpwf1  24336  alexsubALT  24400  tgpconncomp  24462  qustgplem  24470  metequiv2  24859  met2ndci  24871  nrmmetd  24923  nlmvscnlem1  25035  reconn  25178  xrge0tsms  25184  mulc1cncf  25256  ipcnlem1  25596  minveclem3  25780  pmltpc  25801  ovolicc2lem5  25872  ovolicc2  25873  uniioombllem6  25939  dyadmbllem  25950  vitalilem3  25961  mbfmullem  26076  itg2split  26100  itg2mono  26104  bddiblnc  26192  dvlip2  26345  lhop1  26364  dvcnvrelem1  26367  dvfsumrlim  26381  ftc1lem6  26391  itgsubst  26399  dgrco  26624  plyexmo  26666  ulmdvlem3  26759  abelthlem2  26789  abelthlem8  26796  mpodvdsmulf1o  27551  dvdsmulf1o  27553  chpchtsum  27576  dchrptlem2  27622  2sqlem5  27779  2sqlem9  27784  2sqb  27789  chpo1ubb  27838  vmadivsumb  27840  selbergb  27906  selberg2b  27909  selberg3lem2  27915  pntrsumbnd  27923  pntrlog2bnd  27941  pntibndlem3  27949  pnt3  27969  noresle  28084  nosupprefixmo  28087  noinfprefixmo  28088  nosupbday  28092  noinfbday  28107  noinfbnd1lem5  28114  addsprop  28392  mulsproplem9  28540  mulsasslem3  28581  expadds  28851  bdayfinbndlem1  28883  readdscl  28915  tgjustf  28965  hlcgreu  29114  mirreu3  29156  cgraswap  29357  cgracom  29359  cgratr  29360  flatcgra  29362  acopyeu  29372  brprlng  29446  axsegcon  29535  ax5seglem9  29545  axeuclid  29571  axcontlem10  29581  axcontlem12  29583  wwlksnredwwlkn0  30515  n4cyclfrgr  30922  frgrnbnb  30924  numclwwlk1lem2fo  30989  ablo4  31182  smcnlem  31329  pjhthmo  31934  pjpjpre  32051  lnconi  32665  resf1o  33392  mgcoval  33617  xrge0tsmsd  33704  erlval  33889  derangenlem  36103  pconnconn  36163  connpconn  36167  cvmfolem  36211  cvmliftmolem2  36214  cvmliftmo  36216  cvmliftlem7  36223  cvmlift2lem10  36244  cvmlift3lem8  36258  linecgr  37024  btwnconn1lem8  37037  btwnconn1lem14  37043  btwnconn3  37046  brsegle  37051  segletr  37057  segleantisym  37058  outsideofeq  37073  linethru  37096  nadddilem1  37147  finminlem  37284  nn0prpwlem  37288  neibastop2lem  37326  weiunpo  37431  mblfinlem3  38769  ftc1cnnc  38802  isbnd3  38910  cvlcvr1  40588  athgt  40705  4atlem12  40861  paddasslem12  41080  paddasslem13  41081  cdleme0cp  41463  cdleme42keg  41735  cdleme42mgN  41737  trlord  41818  cdlemg6c  41869  cdlemkid4  42183  dihopelvalcpre  42497  dihmeetlem1N  42539  dihglblem5apreN  42540  dihmeetlem4preN  42555  dihmeetlem6  42558  dihmeetlem10N  42565  dihmeetlem11N  42566  dihmeetlem13N  42568  dihjatcclem4  42670  fsuppssind  43814  mzpcl1  43933  mzpcompact2lem  43955  diophin  43976  pell14qrmulcl  44063  pwssplit4  44284  hbtlem2  44318  iunrelexpuztr  44911  stoweidlem57  47272  stoweidlem61  47276  fourierdlem92  47413  euoreqb  48385  prproropf1olem3  48792  prproropf1olem4  48793  fpprwpprb  49043  cycldlenngric  49231  grimgrtri  49252  2zlidl  49542  lmodvsmdi  49696  2arwcat  50943