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 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

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

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 401

This theorem is used by:  fcof1  7285  mpo0  7497  fpr3g  8280  fprresex  8305  eroveu  8808  boxriin  8936  fofinf1o  9287  finsschain  9314  suppeqfsuppbi  9337  fsuppunbi  9347  marypha1lem  9391  wemapsolem  9510  wemapso  9511  wemapso2lem  9512  cantnf  9660  iunfictbso  10105  enfin2i  10311  ttukeylem7  10505  fpwwe2lem2  10623  fpwwe2lem8  10629  fpwwe2lem11  10632  fpwwelem  10636  distrlem4pr  11017  mulcmpblnr  11062  prsrlem1  11063  dedekind  11379  divdivdiv  11922  divmuleq  11926  divadddiv  11936  divsubdiv  11937  lediv12a  12114  xmullem  13296  xlemul1a  13320  seqcaopr  14082  leexp2r  14217  hashf1lem1  14499  hashf1lem2  14500  ccatsymb  14627  wrd2ind  14767  cshweqrep  14865  rtrclreclem4  15105  lo1le  15710  summolem2  15774  summo  15775  prodmolem2  15996  prodmo  15997  bezoutlem3  16605  bezoutlem4  16606  qredeu  16722  pcadd  16955  prmreclem2  16983  vdwlem9  17055  vdwlem10  17056  ramub1lem2  17093  ramub1  17094  prmgaplem7  17123  cofucl  17951  initoeu2  18079  setcmon  18150  poslubmo  18471  posglbmo  18472  rabsubmgmd  18768  issubmd  18870  grprcan  19046  isnsg3  19232  ghmpreima  19314  gaorber  19384  psgneu  19582  odcau  19680  lsmsubm  19729  lsmmod  19751  ablfaclem3  20165  rngpropd  20258  ringpropd  20378  lmodvsmmulgdi  21029  lmodprop2d  21056  lss1d  21095  lindff1  21981  islindf4  21999  assamulgscmlem2  22061  mplcoe1  22199  mplcoe5  22202  evlslem1  22244  mdetunilem7  22786  mdetunilem8  22787  mdetunilem9  22788  mdetuni0  22789  mdetmul  22791  cayhamlem3  23055  ppttop  23175  epttop  23177  cnhaus  23522  isreg2  23545  cncmp  23560  1stcfb  23613  2ndcomap  23626  1stccnp  23630  cldllycmp  23663  1stckgenlem  23721  txcls  23772  ptcnp  23790  txdis1cn  23803  txlly  23804  txnlly  23805  pthaus  23806  txhaus  23815  txkgen  23820  xkohaus  23821  xkococnlem  23827  xkococn  23828  opnfbas  24010  hausflimi  24148  hausflim  24149  hauspwpwf1  24155  alexsubALT  24219  tgpconncomp  24281  qustgplem  24289  metequiv2  24678  met2ndci  24690  nrmmetd  24742  nlmvscnlem1  24854  reconn  24997  xrge0tsms  25003  mulc1cncf  25075  ipcnlem1  25415  minveclem3  25599  pmltpc  25620  ovolicc2lem5  25691  ovolicc2  25692  uniioombllem6  25758  dyadmbllem  25769  vitalilem3  25780  mbfmullem  25895  itg2split  25919  itg2mono  25923  bddiblnc  26012  dvlip2  26165  lhop1  26184  dvcnvrelem1  26187  dvfsumrlim  26201  ftc1lem6  26211  itgsubst  26219  dgrco  26443  plyexmo  26485  ulmdvlem3  26576  abelthlem2  26606  abelthlem8  26613  mpodvdsmulf1o  27369  dvdsmulf1o  27371  chpchtsum  27394  dchrptlem2  27440  2sqlem5  27597  2sqlem9  27602  2sqb  27607  chpo1ubb  27656  vmadivsumb  27658  selbergb  27724  selberg2b  27727  selberg3lem2  27733  pntrsumbnd  27741  pntrlog2bnd  27759  pntibndlem3  27767  pnt3  27787  noresle  27872  nosupprefixmo  27875  noinfprefixmo  27876  nosupbday  27880  noinfbday  27895  noinfbnd1lem5  27902  addsprop  28180  mulsproplem9  28328  mulsasslem3  28369  expadds  28639  bdayfinbndlem1  28671  readdscl  28703  tgjustf  28753  hlcgreu  28901  mirreu3  28942  cgraswap  29142  cgracom  29144  cgratr  29145  flatcgra  29146  acopyeu  29156  brprlng  29199  axsegcon  29288  ax5seglem9  29298  axeuclid  29324  axcontlem10  29334  axcontlem12  29336  wwlksnredwwlkn0  30256  n4cyclfrgr  30653  frgrnbnb  30655  numclwwlk1lem2fo  30720  ablo4  30913  smcnlem  31060  pjhthmo  31665  pjpjpre  31782  lnconi  32396  resf1o  33086  mgcoval  33315  xrge0tsmsd  33402  erlval  33587  derangenlem  35671  pconnconn  35731  connpconn  35735  cvmfolem  35779  cvmliftmolem2  35782  cvmliftmo  35784  cvmliftlem7  35791  cvmlift2lem10  35812  cvmlift3lem8  35826  linecgr  36581  btwnconn1lem8  36594  btwnconn1lem14  36600  btwnconn3  36603  brsegle  36608  segletr  36614  segleantisym  36615  outsideofeq  36630  linethru  36653  nadddilem1  36720  finminlem  36857  nn0prpwlem  36861  neibastop2lem  36899  weiunpo  37004  mblfinlem3  38338  ftc1cnnc  38371  isbnd3  38463  cvlcvr1  40141  athgt  40258  4atlem12  40414  paddasslem12  40633  paddasslem13  40634  cdleme0cp  41016  cdleme42keg  41288  cdleme42mgN  41290  trlord  41371  cdlemg6c  41422  cdlemkid4  41736  dihopelvalcpre  42050  dihmeetlem1N  42092  dihglblem5apreN  42093  dihmeetlem4preN  42108  dihmeetlem6  42111  dihmeetlem10N  42118  dihmeetlem11N  42119  dihmeetlem13N  42121  dihjatcclem4  42223  fsuppssind  43353  prjspner1  43386  mzpcl1  43488  mzpcompact2lem  43510  diophin  43531  pell14qrmulcl  43618  pwssplit4  43844  hbtlem2  43879  iunrelexpuztr  44473  stoweidlem57  46799  stoweidlem61  46803  fourierdlem92  46940  euoreqb  47874  prproropf1olem3  48282  prproropf1olem4  48283  fpprwpprb  48533  cycldlenngric  48721  grimgrtri  48742  2zlidl  49033  lmodvsmdi  49187  2arwcat  50406