Theorem anasss 466

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 419	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 418	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anass  468  anabss3  675  biadanid  822  reximddv3  3150  rspc4v  3605  f1elima  7220  fnfvof  7650  frxp3  8107  oecl  8478  oaass  8502  oen0  8527  oeworde  8534  omabs  8592  oiiniseg  9462  cardinfima  10026  fpwwe2lem11  10570  ltmul12a  12014  eluzp1m1  12795  lbzbi  12871  qreccl  12904  xrlttr  13076  elfzodifsumelfzo  13668  quoremnn0  13794  incexc2  15780  mertens  15828  ndvdsadd  16356  nn0seqcvgd  16516  isprm3  16629  isprm7  16654  pcval  16791  prdsval  17394  evlfcl  18159  ghmqusnsg  19190  ghmquskerlem3  19194  frgpup1  19681  frgpup3lem  19683  ghmcmn  19737  gsumval3  19813  gsumzoppg  19850  ablfaclem2  19994  gsumdixp  20204  rhmpreimaidl  21163  rhmqusnsg  21171  frlmgsum  21657  psrass1lem  21817  psrass1  21849  psdmul  22029  evls1maplmhm  22240  m2cpminvid2  22618  pmatcollpw2lem  22640  chcoeffeqlem  22748  neissex  22990  neiptopnei  22995  dissnlocfin  23392  tx1stc  23513  kqreglem1  23604  xpstopnlem1  23672  alexsublem  23907  metuel2  24429  icoopnst  24812  iocopnst  24813  volcn  25483  mbflimsup  25543  mbflim  25545  itg1addlem4  25576  itg1addlem5  25577  itg1climres  25591  limcflf  25758  dvcobr  25825  dvcobrOLD  25826  dvcnvlem  25856  dvfsumge  25904  mdegmullem  25959  plyeq0lem  26091  plypf1  26093  mtestbdd  26290  mbfulm  26291  fsumdvdscom  27071  muinv  27079  logfaclbnd  27109  logexprlim  27112  dchrinv  27148  lgsval3  27202  2sqmo  27324  rpvmasum2  27399  dchrisum0lem1  27403  dchrisum0  27407  selberg  27435  selberg3lem1  27444  selberg34r  27458  pntsval2  27463  nosupbnd1lem5  27600  noinfbnd1lem5  27615  nocvxminlem  27665  oldbday  27788  peano5uzs  28268  iscgrglt  28417  ercgrg  28420  legso  28502  oppperpex  28656  hpgerlem  28668  trgcopyeu  28709  dfcgra2  28733  inaghl  28748  colinearalg  28813  axeuclid  28866  axcontlem2  28868  axcontlem7  28873  wlkiswwlksupgr2  29780  grpoidinvlem4  30409  ipblnfi  30757  shmodsi  31291  eighmorth  31866  kbass5  32022  kbass6  32023  dmdmd  32202  atom1d  32255  mdsymlem2  32306  mdsymlem3  32307  mdsymlem4  32308  mdsymlem5  32309  fmptco1f1o  32530  2ndresdju  32546  fnpreimac  32568  fsumiunle  32727  s3f1  32841  swrdf1  32851  dfmgc2lem  32894  dfmgc2  32895  pwrssmgc  32899  mgcf1o  32902  chnso  32913  mndlrinvb  32939  mndlactf1  32940  mndractf1  32942  gsummpt2co  32961  gsumwrd2dccatlem  32979  tocyccntz  33074  cycpmconjs  33086  conjga  33100  urpropd  33156  elrgspnlem2  33167  elrgspnlem4  33169  elrgspnsubrunlem2  33172  elrgspnsubrun  33173  erler  33189  rlocaddval  33192  rlocmulval  33193  rlocf1  33197  domnprodn0  33199  rrgsubm  33207  subrdom  33208  isdrng4  33218  suborng  33266  eqgvscpbl  33294  dvdsruasso  33329  nsgmgclem  33355  nsgmgc  33356  nsgqusf1olem2  33358  nsgqusf1olem3  33359  lmhmqusker  33361  intlidl  33364  rhmquskerlem  33369  elrspunidl  33372  elrspunsn  33373  idlinsubrg  33375  rhmimaidl  33376  drngidl  33377  prmidl2  33385  idlmulssprm  33386  isprmidlc  33391  rhmpreimaprmidl  33395  qsidomlem1  33396  qsidomlem2  33397  ssdifidllem  33400  ssdifidlprm  33402  mxidlprm  33414  mxidlirredi  33415  ssmxidllem  33417  opprlidlabs  33429  qsdrngi  33439  rsprprmprmidl  33466  rsprprmprmidlb  33467  rprmirred  33475  rprmirredb  33476  rprmdvdsprod  33478  1arithidom  33481  1arithufdlem3  33490  1arithufdlem4  33491  r1plmhm  33548  r1pquslmic  33549  ply1degltdimlem  33591  ply1degltdim  33592  lindsun  33594  lbsdiflsp0  33595  fedgmullem1  33598  fedgmul  33600  lactlmhm  33603  assalactf1o  33604  extdg1id  33634  fldextrspunlsplem  33641  fldextrspunlsp  33642  minplyirred  33674  algextdeglem8  33687  constrextdg2lem  33711  constrextdg2  33712  constrfiss  33714  constrsdrg  33738  cos9thpiminplylem2  33746  zart0  33842  pstmxmet  33860  ordtconnlem1  33887  esumiun  34057  dya2iocnei  34246  omssubadd  34264  actfunsnf1o  34568  fsum2dsub  34571  reprsuc  34579  reprinfz1  34586  reprpmtf1o  34590  breprexplema  34594  circlemeth  34604  hgt750lemb  34620  cusgr3cyclex  35096  resconn  35206  pibt2  37378  uncf  37566  unccur  37570  fin2so  37574  matunitlindflem1  37583  poimirlem6  37593  poimirlem7  37594  poimirlem25  37612  poimirlem28  37615  poimirlem31  37618  poimirlem32  37619  broucube  37621  ismblfin  37628  mbfposadd  37634  itg2gt0cn  37642  ftc1anclem7  37666  ftc1anc  37668  cover2  37682  indexa  37700  filbcmb  37707  seqpo  37714  incsequz  37715  isbnd2  37750  ghomco  37858  unichnidl  37998  isfldidl  38035  dihvalc  41200  dihvalb  41204  uzindd  41938  aks4d1p8  42048  evlselv  42548  fsuppind  42551  radcnvrat  44276  rexabslelem  45387  rexlimddv2  45794  dvnprodlem2  45918  etransclem46  46251  isgrtri  47915  grlimgrtri  47968  lubeldm2  48917  glbeldm2  48918  thincciso2  49417  aacllem  49763