Theorem anasss 467

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 420	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 419	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 206  df-an 397

This theorem is referenced by:  anass  469  anabss3  673  biadanid  821  rspc4v  3630  f1elima  7264  fnfvof  7689  frxp3  8139  oecl  8539  oaass  8563  oen0  8588  oeworde  8595  omabs  8652  oiiniseg  9530  cardinfima  10094  fpwwe2lem11  10638  ltmul12a  12074  eluzp1m1  12852  lbzbi  12924  qreccl  12957  xrlttr  13123  elfzodifsumelfzo  13702  quoremnn0  13825  incexc2  15788  mertens  15836  ndvdsadd  16357  nn0seqcvgd  16511  isprm3  16624  isprm7  16649  pcval  16781  prdsval  17405  evlfcl  18179  frgpup1  19684  frgpup3lem  19686  ghmcmn  19740  gsumval3  19816  gsumzoppg  19853  ablfaclem2  19997  gsumdixp  20207  frlmgsum  21546  psrass1lemOLD  21712  psrass1lem  21715  psrass1  21744  m2cpminvid2  22477  pmatcollpw2lem  22499  chcoeffeqlem  22607  neissex  22851  neiptopnei  22856  dissnlocfin  23253  tx1stc  23374  kqreglem1  23465  xpstopnlem1  23533  alexsublem  23768  metuel2  24294  icoopnst  24679  iocopnst  24680  volcn  25347  mbflimsup  25407  mbflim  25409  itg1addlem4  25440  itg1addlem4OLD  25441  itg1addlem5  25442  itg1climres  25456  limcflf  25622  dvcobr  25687  dvcnvlem  25717  dvfsumge  25763  mdegmullem  25820  plyeq0lem  25948  plypf1  25950  mtestbdd  26141  mbfulm  26142  fsumdvdscom  26913  muinv  26921  logfaclbnd  26949  logexprlim  26952  dchrinv  26988  lgsval3  27042  2sqmo  27164  rpvmasum2  27239  dchrisum0lem1  27243  dchrisum0  27247  selberg  27275  selberg3lem1  27284  selberg34r  27298  pntsval2  27303  nosupbnd1lem5  27439  noinfbnd1lem5  27454  nocvxminlem  27503  oldbday  27620  iscgrglt  28020  ercgrg  28023  legso  28105  oppperpex  28259  hpgerlem  28271  trgcopyeu  28312  dfcgra2  28336  inaghl  28351  colinearalg  28423  axeuclid  28476  axcontlem2  28478  axcontlem7  28483  wlkiswwlksupgr2  29386  grpoidinvlem4  30015  ipblnfi  30363  shmodsi  30897  eighmorth  31472  kbass5  31628  kbass6  31629  dmdmd  31808  atom1d  31861  mdsymlem2  31912  mdsymlem3  31913  mdsymlem4  31914  mdsymlem5  31915  fmptco1f1o  32112  2ndresdju  32129  fnpreimac  32151  fsumiunle  32290  s3f1  32368  swrdf1  32375  dfmgc2lem  32420  dfmgc2  32421  pwrssmgc  32425  mgcf1o  32428  gsummpt2co  32458  tocyccntz  32561  cycpmconjs  32573  urpropd  32636  isdrng4  32653  suborng  32691  eqgvscpbl  32723  dvdsruasso  32752  nsgmgclem  32784  nsgmgc  32785  nsgqusf1olem2  32787  nsgqusf1olem3  32788  ghmquskerlem3  32793  lmhmqusker  32796  intlidl  32798  rhmpreimaidl  32799  rhmquskerlem  32805  elrspunidl  32808  elrspunsn  32809  idlinsubrg  32811  rhmimaidl  32812  drngidl  32813  prmidl2  32821  idlmulssprm  32822  isprmidlc  32828  rhmpreimaprmidl  32832  qsidomlem1  32833  qsidomlem2  32834  mxidlprm  32848  mxidlirredi  32849  ssmxidllem  32851  opprlidlabs  32861  qsdrngi  32871  r1plmhm  32943  r1pquslmic  32944  ply1degltdimlem  32983  ply1degltdim  32984  lindsun  32986  lbsdiflsp0  32987  fedgmullem1  32990  fedgmul  32992  extdg1id  33018  evls1maplmhm  33037  minplyirred  33047  algextdeglem8  33057  zart0  33145  pstmxmet  33163  ordtconnlem1  33190  esumiun  33378  dya2iocnei  33567  omssubadd  33585  actfunsnf1o  33902  fsum2dsub  33905  reprsuc  33913  reprinfz1  33920  reprpmtf1o  33924  breprexplema  33928  circlemeth  33938  hgt750lemb  33954  cusgr3cyclex  34413  resconn  34523  gg-dvcobr  35462  pibt2  36601  uncf  36770  unccur  36774  fin2so  36778  matunitlindflem1  36787  poimirlem6  36797  poimirlem7  36798  poimirlem25  36816  poimirlem28  36819  poimirlem31  36822  poimirlem32  36823  broucube  36825  ismblfin  36832  mbfposadd  36838  itg2gt0cn  36846  ftc1anclem7  36870  ftc1anc  36872  cover2  36886  indexa  36904  filbcmb  36911  seqpo  36918  incsequz  36919  isbnd2  36954  ghomco  37062  unichnidl  37202  isfldidl  37239  dihvalc  40407  dihvalb  40411  uzindd  41148  aks4d1p8  41258  evlselv  41461  fsuppind  41464  radcnvrat  43375  reximddv3  44142  rexabslelem  44427  rexlimddv2  44838  dvnprodlem2  44962  etransclem46  45295  lubeldm2  47677  glbeldm2  47678  aacllem  47936