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 483	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrl 724	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  6908  mpo0  7095  wfrlem17  7823  eroveu  8242  boxriin  8352  undom  8452  fofinf1o  8645  finsschain  8677  suppeqfsuppbi  8693  fsuppunbi  8700  marypha1lem  8743  wemapsolem  8860  wemapso  8861  wemapso2lem  8862  cantnf  9002  iunfictbso  9386  enfin2i  9589  ttukeylem7  9783  fpwwe2lem2  9900  fpwwe2lem9  9906  fpwwe2lem12  9909  fpwwelem  9913  distrlem4pr  10294  mulcmpblnr  10339  prsrlem1  10340  dedekind  10650  divdivdiv  11189  divmuleq  11193  divadddiv  11203  divsubdiv  11204  lediv12a  11381  xmullem  12507  xlemul1a  12531  seqcaopr  13257  leexp2r  13388  hashf1lem1  13661  hashf1lem2  13662  wrd2ind  13921  cshweqrep  14019  lo1le  14842  summolem2  14906  summo  14907  prodmolem2  15122  prodmo  15123  bezoutlem3  15718  bezoutlem4  15719  qredeu  15831  pcadd  16054  prmreclem2  16082  vdwlem9  16154  vdwlem10  16155  ramub1lem2  16192  ramub1  16193  prmgaplem7  16222  cofucl  16987  initoeu2  17105  setcmon  17176  poslubmo  17585  posglbmo  17586  issubmd  17788  grprcan  17894  isnsg3  18067  ghmpreima  18121  gaorber  18179  psgneu  18365  odcau  18459  lsmsubm  18508  lsmmod  18528  ablfaclem3  18926  ringpropd  19022  lmodvsmmulgdi  19359  lmodprop2d  19386  lss1d  19425  assamulgscmlem2  19817  mplcoe1  19933  mplcoe5  19936  evlslem1  19982  lindff1  20646  islindf4  20664  mdetunilem7  20911  mdetunilem8  20912  mdetunilem9  20913  mdetuni0  20914  mdetmul  20916  cayhamlem3  21179  ppttop  21299  epttop  21301  cnhaus  21646  isreg2  21669  cncmp  21684  1stcfb  21737  2ndcomap  21750  1stccnp  21754  cldllycmp  21787  1stckgenlem  21845  txcls  21896  ptcnp  21914  txdis1cn  21927  txlly  21928  txnlly  21929  pthaus  21930  txhaus  21939  txkgen  21944  xkohaus  21945  xkococnlem  21951  xkococn  21952  opnfbas  22134  hausflimi  22272  hausflim  22273  hauspwpwf1  22279  alexsubALT  22343  tgpconncomp  22404  qustgplem  22412  metequiv2  22803  met2ndci  22815  nrmmetd  22867  nlmvscnlem1  22978  reconn  23119  xrge0tsms  23125  mulc1cncf  23196  ipcnlem1  23531  minveclem3  23715  pmltpc  23734  ovolicc2lem5  23805  ovolicc2  23806  uniioombllem6  23872  dyadmbllem  23883  vitalilem3  23894  mbfmullem  24009  itg2split  24033  itg2mono  24037  dvlip2  24275  lhop1  24294  dvcnvrelem1  24297  dvfsumrlim  24311  ftc1lem6  24321  itgsubst  24329  dgrco  24548  plyexmo  24585  ulmdvlem3  24673  abelthlem2  24703  abelthlem8  24710  dvdsmulf1o  25453  chpchtsum  25477  dchrptlem2  25523  2sqlem5  25680  2sqlem9  25685  2sqb  25690  chpo1ubb  25739  vmadivsumb  25741  selbergb  25807  selberg2b  25810  selberg3lem2  25816  pntrsumbnd  25824  pntrlog2bnd  25842  pntibndlem3  25850  pnt3  25870  tgjustf  25941  hlcgreu  26086  mirreu3  26122  cgraswap  26288  cgracom  26290  cgratr  26291  flatcgra  26292  acopyeu  26303  axsegcon  26396  ax5seglem9  26406  axeuclid  26432  axcontlem10  26442  axcontlem12  26444  wwlksnredwwlkn0  27361  n4cyclfrgr  27762  frgrnbnb  27764  numclwwlk1lem2fo  27829  ablo4  28018  smcnlem  28165  pjhthmo  28770  pjpjpre  28887  lnconi  29501  resf1o  30154  xrge0tsmsd  30503  derangenlem  32027  pconnconn  32087  connpconn  32091  cvmfolem  32135  cvmliftmolem2  32138  cvmliftmo  32140  cvmliftlem7  32147  cvmlift2lem10  32168  cvmlift3lem8  32182  fpr3g  32732  noresle  32810  linecgr  33152  btwnconn1lem8  33165  btwnconn1lem14  33171  btwnconn3  33174  brsegle  33179  segletr  33185  segleantisym  33186  outsideofeq  33201  linethru  33224  finminlem  33276  nn0prpwlem  33280  neibastop2lem  33318  mblfinlem3  34481  bddiblnc  34512  ftc1cnnc  34516  isbnd3  34613  cvlcvr1  36025  athgt  36142  4atlem12  36298  paddasslem12  36517  paddasslem13  36518  cdleme0cp  36900  cdleme42keg  37172  cdleme42mgN  37174  trlord  37255  cdlemg6c  37306  cdlemkid4  37620  dihopelvalcpre  37934  dihmeetlem1N  37976  dihglblem5apreN  37977  dihmeetlem4preN  37992  dihmeetlem6  37995  dihmeetlem10N  38002  dihmeetlem11N  38003  dihmeetlem13N  38005  dihjatcclem4  38107  mzpcl1  38830  mzpcompact2lem  38852  diophin  38873  pell14qrmulcl  38964  pwssplit4  39193  hbtlem2  39228  iunrelexpuztr  39568  stoweidlem57  41904  stoweidlem61  41908  fourierdlem92  42045  euoreqb  42844  prproropf1olem3  43169  prproropf1olem4  43170  fpprwpprb  43407  rabsubmgmd  43560  2zlidl  43703  lmodvsmdi  43930