Theorem simprll 775

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 724	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 206  df-an 396

This theorem is referenced by:  fcof1  7139  mpo0  7338  fpr3g  8072  fprresex  8097  wfrlem17OLD  8127  eroveu  8559  boxriin  8686  undom  8800  fofinf1o  9024  finsschain  9056  suppeqfsuppbi  9072  fsuppunbi  9079  marypha1lem  9122  wemapsolem  9239  wemapso  9240  wemapso2lem  9241  cantnf  9381  iunfictbso  9801  enfin2i  10008  ttukeylem7  10202  fpwwe2lem2  10319  fpwwe2lem8  10325  fpwwe2lem11  10328  fpwwelem  10332  distrlem4pr  10713  mulcmpblnr  10758  prsrlem1  10759  dedekind  11068  divdivdiv  11606  divmuleq  11610  divadddiv  11620  divsubdiv  11621  lediv12a  11798  xmullem  12927  xlemul1a  12951  seqcaopr  13688  leexp2r  13820  hashf1lem1  14096  hashf1lem1OLD  14097  hashf1lem2  14098  ccatsymb  14215  wrd2ind  14364  cshweqrep  14462  rtrclreclem4  14700  lo1le  15291  summolem2  15356  summo  15357  prodmolem2  15573  prodmo  15574  bezoutlem3  16177  bezoutlem4  16178  qredeu  16291  pcadd  16518  prmreclem2  16546  vdwlem9  16618  vdwlem10  16619  ramub1lem2  16656  ramub1  16657  prmgaplem7  16686  cofucl  17519  initoeu2  17647  setcmon  17718  poslubmo  18044  posglbmo  18045  issubmd  18360  grprcan  18528  isnsg3  18703  ghmpreima  18771  gaorber  18829  psgneu  19029  odcau  19124  lsmsubm  19173  lsmmod  19196  ablfaclem3  19605  ringpropd  19736  lmodvsmmulgdi  20073  lmodprop2d  20100  lss1d  20140  lindff1  20937  islindf4  20955  assamulgscmlem2  21014  mplcoe1  21148  mplcoe5  21151  evlslem1  21202  mdetunilem7  21675  mdetunilem8  21676  mdetunilem9  21677  mdetuni0  21678  mdetmul  21680  cayhamlem3  21944  ppttop  22065  epttop  22067  cnhaus  22413  isreg2  22436  cncmp  22451  1stcfb  22504  2ndcomap  22517  1stccnp  22521  cldllycmp  22554  1stckgenlem  22612  txcls  22663  ptcnp  22681  txdis1cn  22694  txlly  22695  txnlly  22696  pthaus  22697  txhaus  22706  txkgen  22711  xkohaus  22712  xkococnlem  22718  xkococn  22719  opnfbas  22901  hausflimi  23039  hausflim  23040  hauspwpwf1  23046  alexsubALT  23110  tgpconncomp  23172  qustgplem  23180  metequiv2  23572  met2ndci  23584  nrmmetd  23636  nlmvscnlem1  23756  reconn  23897  xrge0tsms  23903  mulc1cncf  23974  ipcnlem1  24314  minveclem3  24498  pmltpc  24519  ovolicc2lem5  24590  ovolicc2  24591  uniioombllem6  24657  dyadmbllem  24668  vitalilem3  24679  mbfmullem  24795  itg2split  24819  itg2mono  24823  bddiblnc  24911  dvlip2  25064  lhop1  25083  dvcnvrelem1  25086  dvfsumrlim  25100  ftc1lem6  25110  itgsubst  25118  dgrco  25341  plyexmo  25378  ulmdvlem3  25466  abelthlem2  25496  abelthlem8  25503  dvdsmulf1o  26248  chpchtsum  26272  dchrptlem2  26318  2sqlem5  26475  2sqlem9  26480  2sqb  26485  chpo1ubb  26534  vmadivsumb  26536  selbergb  26602  selberg2b  26605  selberg3lem2  26611  pntrsumbnd  26619  pntrlog2bnd  26637  pntibndlem3  26645  pnt3  26665  tgjustf  26738  hlcgreu  26883  mirreu3  26919  cgraswap  27085  cgracom  27087  cgratr  27088  flatcgra  27089  acopyeu  27099  axsegcon  27198  ax5seglem9  27208  axeuclid  27234  axcontlem10  27244  axcontlem12  27246  wwlksnredwwlkn0  28162  n4cyclfrgr  28556  frgrnbnb  28558  numclwwlk1lem2fo  28623  ablo4  28813  smcnlem  28960  pjhthmo  29565  pjpjpre  29682  lnconi  30296  resf1o  30967  mgcoval  31166  xrge0tsmsd  31219  derangenlem  33033  pconnconn  33093  connpconn  33097  cvmfolem  33141  cvmliftmolem2  33144  cvmliftmo  33146  cvmliftlem7  33153  cvmlift2lem10  33174  cvmlift3lem8  33188  noresle  33827  nosupprefixmo  33830  noinfprefixmo  33831  nosupbday  33835  noinfbday  33850  noinfbnd1lem5  33857  linecgr  34310  btwnconn1lem8  34323  btwnconn1lem14  34329  btwnconn3  34332  brsegle  34337  segletr  34343  segleantisym  34344  outsideofeq  34359  linethru  34382  finminlem  34434  nn0prpwlem  34438  neibastop2lem  34476  mblfinlem3  35743  ftc1cnnc  35776  isbnd3  35869  cvlcvr1  37280  athgt  37397  4atlem12  37553  paddasslem12  37772  paddasslem13  37773  cdleme0cp  38155  cdleme42keg  38427  cdleme42mgN  38429  trlord  38510  cdlemg6c  38561  cdlemkid4  38875  dihopelvalcpre  39189  dihmeetlem1N  39231  dihglblem5apreN  39232  dihmeetlem4preN  39247  dihmeetlem6  39250  dihmeetlem10N  39257  dihmeetlem11N  39258  dihmeetlem13N  39260  dihjatcclem4  39362  fsuppssind  40205  prjspner1  40384  mzpcl1  40467  mzpcompact2lem  40489  diophin  40510  pell14qrmulcl  40601  pwssplit4  40830  hbtlem2  40865  iunrelexpuztr  41216  stoweidlem57  43488  stoweidlem61  43492  fourierdlem92  43629  euoreqb  44488  prproropf1olem3  44845  prproropf1olem4  44846  fpprwpprb  45080  rabsubmgmd  45233  2zlidl  45380  lmodvsmdi  45606