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  3149  rspc4v  3592  f1elima  7192  fnfvof  7622  frxp3  8076  oecl  8447  oaass  8471  oen0  8496  oeworde  8503  omabs  8561  oiiniseg  9414  cardinfima  9983  fpwwe2lem11  10527  ltmul12a  11972  eluzp1m1  12753  lbzbi  12829  qreccl  12862  xrlttr  13034  elfzodifsumelfzo  13626  quoremnn0  13755  incexc2  15740  mertens  15788  ndvdsadd  16316  nn0seqcvgd  16476  isprm3  16589  isprm7  16614  pcval  16751  prdsval  17354  evlfcl  18123  chnso  18525  ghmqusnsg  19189  ghmquskerlem3  19193  frgpup1  19682  frgpup3lem  19684  ghmcmn  19738  gsumval3  19814  gsumzoppg  19851  ablfaclem2  19995  gsumdixp  20232  suborng  20786  rhmpreimaidl  21209  rhmqusnsg  21217  frlmgsum  21704  psrass1lem  21864  psrass1  21896  psdmul  22076  evls1maplmhm  22287  m2cpminvid2  22665  pmatcollpw2lem  22687  chcoeffeqlem  22795  neissex  23037  neiptopnei  23042  dissnlocfin  23439  tx1stc  23560  kqreglem1  23651  xpstopnlem1  23719  alexsublem  23954  metuel2  24475  icoopnst  24858  iocopnst  24859  volcn  25529  mbflimsup  25589  mbflim  25591  itg1addlem4  25622  itg1addlem5  25623  itg1climres  25637  limcflf  25804  dvcobr  25871  dvcobrOLD  25872  dvcnvlem  25902  dvfsumge  25950  mdegmullem  26005  plyeq0lem  26137  plypf1  26139  mtestbdd  26336  mbfulm  26337  fsumdvdscom  27117  muinv  27125  logfaclbnd  27155  logexprlim  27158  dchrinv  27194  lgsval3  27248  2sqmo  27370  rpvmasum2  27445  dchrisum0lem1  27449  dchrisum0  27453  selberg  27481  selberg3lem1  27490  selberg34r  27504  pntsval2  27509  nosupbnd1lem5  27646  noinfbnd1lem5  27661  nocvxminlem  27712  oldbday  27841  peano5uzs  28323  iscgrglt  28487  ercgrg  28490  legso  28572  oppperpex  28726  hpgerlem  28738  trgcopyeu  28779  dfcgra2  28803  inaghl  28818  colinearalg  28883  axeuclid  28936  axcontlem2  28938  axcontlem7  28943  wlkiswwlksupgr2  29850  grpoidinvlem4  30479  ipblnfi  30827  shmodsi  31361  eighmorth  31936  kbass5  32092  kbass6  32093  dmdmd  32272  atom1d  32325  mdsymlem2  32376  mdsymlem3  32377  mdsymlem4  32378  mdsymlem5  32379  fmptco1f1o  32607  2ndresdju  32623  fnpreimac  32645  fsumiunle  32804  s3f1  32920  swrdf1  32929  dfmgc2lem  32968  dfmgc2  32969  pwrssmgc  32973  mgcf1o  32976  mndlrinvb  32998  mndlactf1  32999  mndractf1  33001  gsummpt2co  33020  gsumwrd2dccatlem  33038  tocyccntz  33105  cycpmconjs  33117  conjga  33131  fxpsubrg  33135  urpropd  33191  elrgspnlem2  33202  elrgspnlem4  33204  elrgspnsubrunlem2  33207  elrgspnsubrun  33208  erler  33224  rlocaddval  33227  rlocmulval  33228  rlocf1  33232  domnprodn0  33234  rrgsubm  33242  subrdom  33243  isdrng4  33253  eqgvscpbl  33307  dvdsruasso  33342  nsgmgclem  33368  nsgmgc  33369  nsgqusf1olem2  33371  nsgqusf1olem3  33372  lmhmqusker  33374  intlidl  33377  rhmquskerlem  33382  elrspunidl  33385  elrspunsn  33386  idlinsubrg  33388  rhmimaidl  33389  drngidl  33390  prmidl2  33398  idlmulssprm  33399  isprmidlc  33404  rhmpreimaprmidl  33408  qsidomlem1  33409  qsidomlem2  33410  ssdifidllem  33413  ssdifidlprm  33415  mxidlprm  33427  mxidlirredi  33428  ssmxidllem  33430  opprlidlabs  33442  qsdrngi  33452  rsprprmprmidl  33479  rsprprmprmidlb  33480  rprmirred  33488  rprmirredb  33489  rprmdvdsprod  33491  1arithidom  33494  1arithufdlem3  33503  1arithufdlem4  33504  r1plmhm  33562  r1pquslmic  33563  mplvrpmga  33567  mplvrpmmhm  33568  mplvrpmrhm  33569  ply1degltdimlem  33627  ply1degltdim  33628  lindsun  33630  lbsdiflsp0  33631  fedgmullem1  33634  fedgmul  33636  lactlmhm  33639  assalactf1o  33640  extdg1id  33671  fldextrspunlsplem  33678  fldextrspunlsp  33679  extdgfialglem2  33698  extdgfialg  33699  minplyirred  33716  algextdeglem8  33729  constrextdg2lem  33753  constrextdg2  33754  constrfiss  33756  constrsdrg  33780  cos9thpiminplylem2  33788  zart0  33884  pstmxmet  33902  ordtconnlem1  33929  esumiun  34099  dya2iocnei  34287  omssubadd  34305  actfunsnf1o  34609  fsum2dsub  34612  reprsuc  34620  reprinfz1  34627  reprpmtf1o  34631  breprexplema  34635  circlemeth  34645  hgt750lemb  34661  cusgr3cyclex  35172  resconn  35282  pibt2  37451  uncf  37639  unccur  37643  fin2so  37647  matunitlindflem1  37656  poimirlem6  37666  poimirlem7  37667  poimirlem25  37685  poimirlem28  37688  poimirlem31  37691  poimirlem32  37692  broucube  37694  ismblfin  37701  mbfposadd  37707  itg2gt0cn  37715  ftc1anclem7  37739  ftc1anc  37741  cover2  37755  indexa  37773  filbcmb  37780  seqpo  37787  incsequz  37788  isbnd2  37823  ghomco  37931  unichnidl  38071  isfldidl  38108  dihvalc  41272  dihvalb  41276  uzindd  42010  aks4d1p8  42120  evlselv  42620  fsuppind  42623  radcnvrat  44347  rexabslelem  45456  rexlimddv2  45861  dvnprodlem2  45985  etransclem46  46318  isgrtri  47974  grlimgrtri  48034  lubeldm2  48987  glbeldm2  48988  thincciso2  49487  aacllem  49833