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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  fcof1  7287  mpo0  7496  fpr3g  8272  fprresex  8297  wfrlem17OLD  8327  eroveu  8808  boxriin  8936  undomOLD  9062  fofinf1o  9329  finsschain  9361  suppeqfsuppbi  9379  fsuppunbi  9386  marypha1lem  9430  wemapsolem  9547  wemapso  9548  wemapso2lem  9549  cantnf  9690  iunfictbso  10111  enfin2i  10318  ttukeylem7  10512  fpwwe2lem2  10629  fpwwe2lem8  10635  fpwwe2lem11  10638  fpwwelem  10642  distrlem4pr  11023  mulcmpblnr  11068  prsrlem1  11069  dedekind  11381  divdivdiv  11919  divmuleq  11923  divadddiv  11933  divsubdiv  11934  lediv12a  12111  xmullem  13247  xlemul1a  13271  seqcaopr  14009  leexp2r  14143  hashf1lem1  14419  hashf1lem1OLD  14420  hashf1lem2  14421  ccatsymb  14536  wrd2ind  14677  cshweqrep  14775  rtrclreclem4  15012  lo1le  15602  summolem2  15666  summo  15667  prodmolem2  15883  prodmo  15884  bezoutlem3  16487  bezoutlem4  16488  qredeu  16599  pcadd  16826  prmreclem2  16854  vdwlem9  16926  vdwlem10  16927  ramub1lem2  16964  ramub1  16965  prmgaplem7  16994  cofucl  17842  initoeu2  17970  setcmon  18041  poslubmo  18368  posglbmo  18369  rabsubmgmd  18629  issubmd  18723  grprcan  18894  isnsg3  19076  ghmpreima  19152  gaorber  19213  psgneu  19415  odcau  19513  lsmsubm  19562  lsmmod  19584  ablfaclem3  19998  rngpropd  20068  ringpropd  20176  lmodvsmmulgdi  20651  lmodprop2d  20678  lss1d  20718  lindff1  21594  islindf4  21612  assamulgscmlem2  21673  mplcoe1  21811  mplcoe5  21814  evlslem1  21864  mdetunilem7  22340  mdetunilem8  22341  mdetunilem9  22342  mdetuni0  22343  mdetmul  22345  cayhamlem3  22609  ppttop  22730  epttop  22732  cnhaus  23078  isreg2  23101  cncmp  23116  1stcfb  23169  2ndcomap  23182  1stccnp  23186  cldllycmp  23219  1stckgenlem  23277  txcls  23328  ptcnp  23346  txdis1cn  23359  txlly  23360  txnlly  23361  pthaus  23362  txhaus  23371  txkgen  23376  xkohaus  23377  xkococnlem  23383  xkococn  23384  opnfbas  23566  hausflimi  23704  hausflim  23705  hauspwpwf1  23711  alexsubALT  23775  tgpconncomp  23837  qustgplem  23845  metequiv2  24239  met2ndci  24251  nrmmetd  24303  nlmvscnlem1  24423  reconn  24564  xrge0tsms  24570  mulc1cncf  24645  ipcnlem1  24993  minveclem3  25177  pmltpc  25199  ovolicc2lem5  25270  ovolicc2  25271  uniioombllem6  25337  dyadmbllem  25348  vitalilem3  25359  mbfmullem  25475  itg2split  25499  itg2mono  25503  bddiblnc  25591  dvlip2  25747  lhop1  25766  dvcnvrelem1  25769  dvfsumrlim  25783  ftc1lem6  25793  itgsubst  25801  dgrco  26025  plyexmo  26062  ulmdvlem3  26150  abelthlem2  26180  abelthlem8  26187  dvdsmulf1o  26934  chpchtsum  26958  dchrptlem2  27004  2sqlem5  27161  2sqlem9  27166  2sqb  27171  chpo1ubb  27220  vmadivsumb  27222  selbergb  27288  selberg2b  27291  selberg3lem2  27297  pntrsumbnd  27305  pntrlog2bnd  27323  pntibndlem3  27331  pnt3  27351  noresle  27436  nosupprefixmo  27439  noinfprefixmo  27440  nosupbday  27444  noinfbday  27459  noinfbnd1lem5  27466  addsprop  27698  mulsproplem9  27819  mulsasslem3  27859  tgjustf  27991  hlcgreu  28136  mirreu3  28172  cgraswap  28338  cgracom  28340  cgratr  28341  flatcgra  28342  acopyeu  28352  axsegcon  28452  ax5seglem9  28462  axeuclid  28488  axcontlem10  28498  axcontlem12  28500  wwlksnredwwlkn0  29417  n4cyclfrgr  29811  frgrnbnb  29813  numclwwlk1lem2fo  29878  ablo4  30070  smcnlem  30217  pjhthmo  30822  pjpjpre  30939  lnconi  31553  resf1o  32222  mgcoval  32423  xrge0tsmsd  32479  derangenlem  34460  pconnconn  34520  connpconn  34524  cvmfolem  34568  cvmliftmolem2  34571  cvmliftmo  34573  cvmliftlem7  34580  cvmlift2lem10  34601  cvmlift3lem8  34615  linecgr  35357  btwnconn1lem8  35370  btwnconn1lem14  35376  btwnconn3  35379  brsegle  35384  segletr  35390  segleantisym  35391  outsideofeq  35406  linethru  35429  finminlem  35506  nn0prpwlem  35510  neibastop2lem  35548  mblfinlem3  36830  ftc1cnnc  36863  isbnd3  36955  cvlcvr1  38512  athgt  38630  4atlem12  38786  paddasslem12  39005  paddasslem13  39006  cdleme0cp  39388  cdleme42keg  39660  cdleme42mgN  39662  trlord  39743  cdlemg6c  39794  cdlemkid4  40108  dihopelvalcpre  40422  dihmeetlem1N  40464  dihglblem5apreN  40465  dihmeetlem4preN  40480  dihmeetlem6  40483  dihmeetlem10N  40490  dihmeetlem11N  40491  dihmeetlem13N  40493  dihjatcclem4  40595  fsuppssind  41467  prjspner1  41670  mzpcl1  41769  mzpcompact2lem  41791  diophin  41812  pell14qrmulcl  41903  pwssplit4  42133  hbtlem2  42168  iunrelexpuztr  42772  stoweidlem57  45071  stoweidlem61  45075  fourierdlem92  45212  euoreqb  46115  prproropf1olem3  46471  prproropf1olem4  46472  fpprwpprb  46706  2zlidl  46920  lmodvsmdi  47146