Theorem anasss 470

Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
anasss.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
anasss	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem anasss

Step	Hyp	Ref	Expression
1		anasss.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
2	1	exp31 423	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 422	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anass  472  anabss3  685  biadanid  832  reximddv3  3178  rspc4v  3600  f1elima  7242  fnfvof  7672  frxp3  8125  oecl  8500  oaass  8524  oen0  8550  oeworde  8557  omabs  8615  oiiniseg  9475  cardinfima  10047  fpwwe2lem11  10593  ltmul12a  12041  eluzp1m1  12859  lbzbi  12931  qreccl  12964  xrlttr  13136  elfzodifsumelfzo  13731  quoremnn0  13860  incexc2  15859  mertens  15907  ndvdsadd  16435  nn0seqcvgd  16595  isprm3  16708  isprm7  16734  pcval  16871  prdsval  17475  evlfcl  18245  chnso  18647  ghmqusnsg  19313  ghmquskerlem3  19317  frgpup1  19806  frgpup3lem  19808  ghmcmn  19862  gsumval3  19938  gsumzoppg  19975  ablfaclem2  20119  gsumdixp  20354  suborng  20913  rhmpreimaidl  21335  rhmqusnsg  21343  frlmgsum  21812  psrass1lem  21973  psrass1  22003  psdmul  22219  evls1maplmhm  22428  m2cpminvid2  22803  pmatcollpw2lem  22825  chcoeffeqlem  22933  neissex  23175  neiptopnei  23180  dissnlocfin  23577  tx1stc  23698  kqreglem1  23789  xpstopnlem1  23857  alexsublem  24092  metuel2  24613  icoopnst  24989  iocopnst  24990  volcn  25656  mbflimsup  25716  mbflim  25718  itg1addlem4  25749  itg1addlem5  25750  itg1climres  25764  limcflf  25931  dvcobr  25996  dvcnvlem  26026  dvfsumge  26072  mdegmullem  26126  plyeq0lem  26258  plypf1  26260  mtestbdd  26456  mbfulm  26457  fsumdvdscom  27237  muinv  27245  logfaclbnd  27274  logexprlim  27277  dchrinv  27313  lgsval3  27367  2sqmo  27489  rpvmasum2  27564  dchrisum0lem1  27568  dchrisum0  27572  selberg  27600  selberg3lem1  27609  selberg34r  27623  pntsval2  27628  nosupbnd1lem5  27764  noinfbnd1lem5  27779  nocvxminlem  27835  oldbday  27982  peano5uzs  28485  iscgrglt  28671  ercgrg  28674  legso  28756  oppperpex  28910  hpgerlem  28922  trgcopyeu  28963  dfcgra2  28987  inaghl  29002  colinearalg  29068  axeuclid  29121  axcontlem2  29123  axcontlem7  29128  wlkiswwlksupgr2  30034  grpoidinvlem4  30667  ipblnfi  31015  shmodsi  31549  eighmorth  32124  kbass5  32280  kbass6  32281  dmdmd  32460  atom1d  32513  mdsymlem2  32564  mdsymlem3  32565  mdsymlem4  32566  mdsymlem5  32567  fmptco1f1o  32796  2ndresdju  32812  fnpreimac  32833  fsumiunle  32992  s3f1  33086  swrdf1  33095  dfmgc2lem  33134  dfmgc2  33135  pwrssmgc  33139  mgcf1o  33142  mndlrinvb  33164  mndlactf1  33165  mndractf1  33167  gsummpt2co  33189  gsumwrd2dccatlem  33218  tocyccntz  33285  cycpmconjs  33297  conjga  33311  fxpsubrg  33315  urpropd  33372  elrgspnlem2  33385  elrgspnlem4  33387  elrgspnsubrunlem2  33390  elrgspnsubrun  33391  erler  33407  rlocaddval  33411  rlocmulval  33412  rlocf1  33416  domnprodn0  33420  domnprodeq0  33421  rrgsubm  33429  subrdom  33430  ricdomn1  33434  isdrng4  33443  eqgvscpbl  33497  dvdsruasso  33532  nsgmgclem  33558  nsgmgc  33559  nsgqusf1olem2  33561  nsgqusf1olem3  33562  lmhmqusker  33564  intlidl  33567  rhmquskerlem  33572  elrspunidl  33575  elrspunsn  33576  idlinsubrg  33578  rhmimaidl  33579  drngidl  33580  prmidl2  33588  idlmulssprm  33589  isprmidlc  33594  rhmpreimaprmidl  33599  qsidomlem1  33600  qsidomlem2  33601  ssdifidllem  33604  ssdifidlprm  33606  prmidlsubm  33607  mxidlprm  33619  mxidlirredi  33620  ssmxidllem  33622  opprlidlabs  33634  qsdrngi  33644  drnglring  33649  dflringlem2  33652  rsprprmprmidl  33679  rsprprmprmidlb  33680  rprmirred  33688  rprmirredb  33689  rprmdvdsprod  33691  1arithidom  33694  1arithufdlem3  33703  1arithufdlem4  33704  deg1prod  33740  r1plmhm  33767  r1pquslmic  33768  0mplrim  33772  selvply1rhmlema  33776  selvply1rhmlem1  33778  selvply1rhm  33783  mplidomlem  33785  extvfvcl  33794  mplvrpmga  33803  mplvrpmmhm  33804  mplvrpmrhm  33805  psrgsum  33806  psrmonprod  33810  esplyfval1  33831  esplyfvaln  33832  vieta  33838  ply1degltdimlem  33880  ply1degltdim  33881  lindsun  33883  lbsdiflsp0  33884  fedgmullem1  33887  fedgmul  33889  lactlmhm  33892  assalactf1o  33893  extdg1id  33924  fldextrspunlsplem  33931  fldextrspunlsp  33932  extdgfialglem2  33951  extdgfialg  33952  minplyirred  33969  algextdeglem8  33982  constrextdg2lem  34006  constrextdg2  34007  constrfiss  34009  constrsdrg  34033  cos9thpiminplylem2  34041  zart0  34137  pstmxmet  34155  ordtconnlem1  34182  esumiun  34352  dya2iocnei  34540  omssubadd  34558  actfunsnf1o  34859  fsum2dsub  34862  reprsuc  34870  reprinfz1  34877  reprpmtf1o  34881  breprexplema  34885  circlemeth  34895  hgt750lemb  34911  cusgr3cyclex  35447  resconn  35557  pibt2  37872  uncf  38059  unccur  38063  fin2so  38067  matunitlindflem1  38076  poimirlem6  38086  poimirlem7  38087  poimirlem25  38105  poimirlem28  38108  poimirlem31  38111  poimirlem32  38112  broucube  38114  ismblfin  38121  mbfposadd  38127  itg2gt0cn  38135  ftc1anclem7  38159  ftc1anc  38161  cover2  38175  indexa  38193  filbcmb  38200  seqpo  38207  incsequz  38208  isbnd2  38243  ghomco  38351  unichnidl  38491  isfldidl  38528  dihvalc  41818  dihvalb  41822  uzindd  42556  aks4d1p8  42665  evlselv  43132  fsuppind  43133  radcnvrat  44851  rexabslelem  45953  rexlimddv2  46358  dvnprodlem2  46482  etransclem46  46815  isgrtri  48526  grlimgrtri  48586  lubeldm2  49538  glbeldm2  49539  thincciso2  50037  aacllem  50383