Theorem simprll 784

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  fcof1  7238  mpo0  7448  fpr3g  8232  fprresex  8257  eroveu  8756  boxriin  8885  fofinf1o  9239  finsschain  9266  suppeqfsuppbi  9289  fsuppunbi  9299  marypha1lem  9343  wemapsolem  9462  wemapso  9463  wemapso2lem  9464  cantnf  9612  iunfictbso  10034  enfin2i  10241  ttukeylem7  10435  fpwwe2lem2  10553  fpwwe2lem8  10559  fpwwe2lem11  10562  fpwwelem  10566  distrlem4pr  10947  mulcmpblnr  10992  prsrlem1  10993  dedekind  11307  divdivdiv  11854  divmuleq  11858  divadddiv  11868  divsubdiv  11869  lediv12a  12047  xmullem  13214  xlemul1a  13238  seqcaopr  13999  leexp2r  14134  hashf1lem1  14415  hashf1lem2  14416  ccatsymb  14543  wrd2ind  14683  cshweqrep  14781  rtrclreclem4  15021  lo1le  15612  summolem2  15676  summo  15677  prodmolem2  15898  prodmo  15899  bezoutlem3  16508  bezoutlem4  16509  qredeu  16625  pcadd  16858  prmreclem2  16886  vdwlem9  16958  vdwlem10  16959  ramub1lem2  16996  ramub1  16997  prmgaplem7  17026  cofucl  17853  initoeu2  17981  setcmon  18052  poslubmo  18373  posglbmo  18374  rabsubmgmd  18670  issubmd  18772  grprcan  18947  isnsg3  19133  ghmpreima  19211  gaorber  19281  psgneu  19479  odcau  19577  lsmsubm  19626  lsmmod  19648  ablfaclem3  20062  rngpropd  20153  ringpropd  20267  lmodvsmmulgdi  20894  lmodprop2d  20921  lss1d  20960  lindff1  21802  islindf4  21820  assamulgscmlem2  21882  mplcoe1  22020  mplcoe5  22023  evlslem1  22065  mdetunilem7  22608  mdetunilem8  22609  mdetunilem9  22610  mdetuni0  22611  mdetmul  22613  cayhamlem3  22877  ppttop  22997  epttop  22999  cnhaus  23344  isreg2  23367  cncmp  23382  1stcfb  23435  2ndcomap  23448  1stccnp  23452  cldllycmp  23485  1stckgenlem  23543  txcls  23594  ptcnp  23612  txdis1cn  23625  txlly  23626  txnlly  23627  pthaus  23628  txhaus  23637  txkgen  23642  xkohaus  23643  xkococnlem  23649  xkococn  23650  opnfbas  23832  hausflimi  23970  hausflim  23971  hauspwpwf1  23977  alexsubALT  24041  tgpconncomp  24103  qustgplem  24111  metequiv2  24500  met2ndci  24512  nrmmetd  24564  nlmvscnlem1  24676  reconn  24819  xrge0tsms  24825  mulc1cncf  24897  ipcnlem1  25237  minveclem3  25421  pmltpc  25442  ovolicc2lem5  25513  ovolicc2  25514  uniioombllem6  25580  dyadmbllem  25591  vitalilem3  25602  mbfmullem  25717  itg2split  25741  itg2mono  25745  bddiblnc  25834  dvlip2  25987  lhop1  26006  dvcnvrelem1  26009  dvfsumrlim  26023  ftc1lem6  26033  itgsubst  26041  dgrco  26265  plyexmo  26304  ulmdvlem3  26392  abelthlem2  26422  abelthlem8  26429  mpodvdsmulf1o  27182  dvdsmulf1o  27184  chpchtsum  27207  dchrptlem2  27253  2sqlem5  27410  2sqlem9  27415  2sqb  27420  chpo1ubb  27469  vmadivsumb  27471  selbergb  27537  selberg2b  27540  selberg3lem2  27546  pntrsumbnd  27554  pntrlog2bnd  27572  pntibndlem3  27580  pnt3  27600  noresle  27686  nosupprefixmo  27689  noinfprefixmo  27690  nosupbday  27694  noinfbday  27709  noinfbnd1lem5  27716  addsprop  27993  mulsproplem9  28141  mulsasslem3  28182  expadds  28452  bdayfinbndlem1  28484  readdscl  28516  tgjustf  28566  hlcgreu  28711  mirreu3  28747  cgraswap  28913  cgracom  28915  cgratr  28916  flatcgra  28917  acopyeu  28927  axsegcon  29021  ax5seglem9  29031  axeuclid  29057  axcontlem10  29067  axcontlem12  29069  wwlksnredwwlkn0  29989  n4cyclfrgr  30386  frgrnbnb  30388  numclwwlk1lem2fo  30453  ablo4  30646  smcnlem  30793  pjhthmo  31398  pjpjpre  31515  lnconi  32129  resf1o  32829  mgcoval  33072  xrge0tsmsd  33161  erlval  33346  derangenlem  35400  pconnconn  35460  connpconn  35464  cvmfolem  35508  cvmliftmolem2  35511  cvmliftmo  35513  cvmliftlem7  35520  cvmlift2lem10  35541  cvmlift3lem8  35555  linecgr  36310  btwnconn1lem8  36323  btwnconn1lem14  36329  btwnconn3  36332  brsegle  36337  segletr  36343  segleantisym  36344  outsideofeq  36359  linethru  36382  finminlem  36547  nn0prpwlem  36551  neibastop2lem  36589  weiunpo  36694  mblfinlem3  38027  ftc1cnnc  38060  isbnd3  38152  cvlcvr1  39832  athgt  39949  4atlem12  40105  paddasslem12  40324  paddasslem13  40325  cdleme0cp  40707  cdleme42keg  40979  cdleme42mgN  40981  trlord  41062  cdlemg6c  41113  cdlemkid4  41427  dihopelvalcpre  41741  dihmeetlem1N  41783  dihglblem5apreN  41784  dihmeetlem4preN  41799  dihmeetlem6  41802  dihmeetlem10N  41809  dihmeetlem11N  41810  dihmeetlem13N  41812  dihjatcclem4  41914  fsuppssind  43044  prjspner1  43077  mzpcl1  43179  mzpcompact2lem  43201  diophin  43222  pell14qrmulcl  43309  pwssplit4  43535  hbtlem2  43570  iunrelexpuztr  44164  stoweidlem57  46501  stoweidlem61  46505  fourierdlem92  46642  euoreqb  47573  prproropf1olem3  47981  prproropf1olem4  47982  fpprwpprb  48232  cycldlenngric  48420  grimgrtri  48441  2zlidl  48732  lmodvsmdi  48871  2arwcat  50091