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  7283  mpo0  7493  fpr3g  8281  fprresex  8306  eroveu  8811  boxriin  8946  fofinf1o  9299  finsschain  9326  suppeqfsuppbi  9349  fsuppunbi  9359  marypha1lem  9403  wemapsolem  9522  wemapso  9523  wemapso2lem  9524  cantnf  9672  iunfictbso  10165  enfin2i  10371  ttukeylem7  10565  fpwwe2lem2  10689  fpwwe2lem8  10695  fpwwe2lem11  10698  fpwwelem  10702  distrlem4pr  11083  mulcmpblnr  11128  prsrlem1  11129  dedekind  11445  divdivdiv  11988  divmuleq  11992  divadddiv  12002  divsubdiv  12003  lediv12a  12180  xmullem  13364  xlemul1a  13388  seqcaopr  14151  leexp2r  14286  hashf1lem1  14568  hashf1lem2  14569  ccatsymb  14696  wrd2ind  14840  cshweqrep  14940  rtrclreclem4  15182  lo1le  15787  summolem2  15850  summo  15851  prodmolem2  16070  prodmo  16071  bezoutlem3  16679  bezoutlem4  16680  qredeu  16796  pcadd  17029  prmreclem2  17057  vdwlem9  17129  vdwlem10  17130  ramub1lem2  17167  ramub1  17168  prmgaplem7  17197  cofucl  18025  initoeu2  18153  setcmon  18224  poslubmo  18545  posglbmo  18546  rabsubmgmd  18855  issubmd  18963  grprcan  19146  isnsg3  19332  ghmpreima  19414  gaorber  19484  psgneu  19682  odcau  19780  lsmsubm  19829  lsmmod  19851  ablfaclem3  20265  rngpropd  20358  ringpropd  20481  lmodvsmmulgdi  21134  lmodprop2d  21161  lss1d  21200  lindff1  22088  islindf4  22106  assamulgscmlem2  22170  mplcoe1  22308  mplcoe5  22311  evlslem1  22353  mdetunilem7  22895  mdetunilem8  22896  mdetunilem9  22897  mdetuni0  22898  mdetmul  22900  cayhamlem3  23167  ppttop  23287  epttop  23289  cnhaus  23634  isreg2  23657  cncmp  23672  1stcfb  23725  2ndcomap  23739  1stccnp  23743  cldllycmp  23776  1stckgenlem  23834  txcls  23885  ptcnp  23903  txdis1cn  23916  txlly  23917  txnlly  23918  pthaus  23919  txhaus  23928  txkgen  23933  xkohaus  23934  xkococnlem  23940  xkococn  23941  opnfbas  24123  hausflimi  24261  hausflim  24262  hauspwpwf1  24268  alexsubALT  24332  tgpconncomp  24394  qustgplem  24402  metequiv2  24791  met2ndci  24803  nrmmetd  24855  nlmvscnlem1  24967  reconn  25110  xrge0tsms  25116  mulc1cncf  25188  ipcnlem1  25528  minveclem3  25712  pmltpc  25733  ovolicc2lem5  25804  ovolicc2  25805  uniioombllem6  25871  dyadmbllem  25882  vitalilem3  25893  mbfmullem  26008  itg2split  26032  itg2mono  26036  bddiblnc  26124  dvlip2  26277  lhop1  26296  dvcnvrelem1  26299  dvfsumrlim  26313  ftc1lem6  26323  itgsubst  26331  dgrco  26556  plyexmo  26600  ulmdvlem3  26693  abelthlem2  26723  abelthlem8  26730  mpodvdsmulf1o  27485  dvdsmulf1o  27487  chpchtsum  27510  dchrptlem2  27556  2sqlem5  27713  2sqlem9  27718  2sqb  27723  chpo1ubb  27772  vmadivsumb  27774  selbergb  27840  selberg2b  27843  selberg3lem2  27849  pntrsumbnd  27857  pntrlog2bnd  27875  pntibndlem3  27883  pnt3  27903  noresle  27988  nosupprefixmo  27991  noinfprefixmo  27992  nosupbday  27996  noinfbday  28011  noinfbnd1lem5  28018  addsprop  28296  mulsproplem9  28444  mulsasslem3  28485  expadds  28755  bdayfinbndlem1  28787  readdscl  28819  tgjustf  28869  hlcgreu  29018  mirreu3  29060  cgraswap  29261  cgracom  29263  cgratr  29264  flatcgra  29266  acopyeu  29276  brprlng  29350  axsegcon  29439  ax5seglem9  29449  axeuclid  29475  axcontlem10  29485  axcontlem12  29487  wwlksnredwwlkn0  30419  n4cyclfrgr  30826  frgrnbnb  30828  numclwwlk1lem2fo  30893  ablo4  31086  smcnlem  31233  pjhthmo  31838  pjpjpre  31955  lnconi  32569  resf1o  33256  mgcoval  33481  xrge0tsmsd  33568  erlval  33753  derangenlem  35857  pconnconn  35917  connpconn  35921  cvmfolem  35965  cvmliftmolem2  35968  cvmliftmo  35970  cvmliftlem7  35977  cvmlift2lem10  35998  cvmlift3lem8  36012  linecgr  36768  btwnconn1lem8  36781  btwnconn1lem14  36787  btwnconn3  36790  brsegle  36795  segletr  36801  segleantisym  36802  outsideofeq  36817  linethru  36840  nadddilem1  36891  finminlem  37028  nn0prpwlem  37032  neibastop2lem  37070  weiunpo  37175  mblfinlem3  38497  ftc1cnnc  38530  isbnd3  38638  cvlcvr1  40316  athgt  40433  4atlem12  40589  paddasslem12  40808  paddasslem13  40809  cdleme0cp  41191  cdleme42keg  41463  cdleme42mgN  41465  trlord  41546  cdlemg6c  41597  cdlemkid4  41911  dihopelvalcpre  42225  dihmeetlem1N  42267  dihglblem5apreN  42268  dihmeetlem4preN  42283  dihmeetlem6  42286  dihmeetlem10N  42293  dihmeetlem11N  42294  dihmeetlem13N  42296  dihjatcclem4  42398  fsuppssind  43543  prjspner1  43576  mzpcl1  43678  mzpcompact2lem  43700  diophin  43721  pell14qrmulcl  43808  pwssplit4  44034  hbtlem2  44069  iunrelexpuztr  44663  stoweidlem57  46989  stoweidlem61  46993  fourierdlem92  47130  euoreqb  48101  prproropf1olem3  48509  prproropf1olem4  48510  fpprwpprb  48760  cycldlenngric  48948  grimgrtri  48969  2zlidl  49259  lmodvsmdi  49413  2arwcat  50630