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  823  reximddv3  3172  rspc4v  3642  f1elima  7283  fnfvof  7714  frxp3  8176  oecl  8575  oaass  8599  oen0  8624  oeworde  8631  omabs  8689  oiiniseg  9573  cardinfima  10137  fpwwe2lem11  10681  ltmul12a  12123  eluzp1m1  12904  lbzbi  12978  qreccl  13011  xrlttr  13182  elfzodifsumelfzo  13770  quoremnn0  13896  incexc2  15874  mertens  15922  ndvdsadd  16447  nn0seqcvgd  16607  isprm3  16720  isprm7  16745  pcval  16882  prdsval  17500  evlfcl  18267  ghmqusnsg  19300  ghmquskerlem3  19304  frgpup1  19793  frgpup3lem  19795  ghmcmn  19849  gsumval3  19925  gsumzoppg  19962  ablfaclem2  20106  gsumdixp  20316  rhmpreimaidl  21287  rhmqusnsg  21295  frlmgsum  21792  psrass1lem  21952  psrass1  21984  psdmul  22170  evls1maplmhm  22381  m2cpminvid2  22761  pmatcollpw2lem  22783  chcoeffeqlem  22891  neissex  23135  neiptopnei  23140  dissnlocfin  23537  tx1stc  23658  kqreglem1  23749  xpstopnlem1  23817  alexsublem  24052  metuel2  24578  icoopnst  24969  iocopnst  24970  volcn  25641  mbflimsup  25701  mbflim  25703  itg1addlem4  25734  itg1addlem5  25735  itg1climres  25749  limcflf  25916  dvcobr  25983  dvcobrOLD  25984  dvcnvlem  26014  dvfsumge  26062  mdegmullem  26117  plyeq0lem  26249  plypf1  26251  mtestbdd  26448  mbfulm  26449  fsumdvdscom  27228  muinv  27236  logfaclbnd  27266  logexprlim  27269  dchrinv  27305  lgsval3  27359  2sqmo  27481  rpvmasum2  27556  dchrisum0lem1  27560  dchrisum0  27564  selberg  27592  selberg3lem1  27601  selberg34r  27615  pntsval2  27620  nosupbnd1lem5  27757  noinfbnd1lem5  27772  nocvxminlem  27822  oldbday  27939  peano5uzs  28390  iscgrglt  28522  ercgrg  28525  legso  28607  oppperpex  28761  hpgerlem  28773  trgcopyeu  28814  dfcgra2  28838  inaghl  28853  colinearalg  28925  axeuclid  28978  axcontlem2  28980  axcontlem7  28985  wlkiswwlksupgr2  29897  grpoidinvlem4  30526  ipblnfi  30874  shmodsi  31408  eighmorth  31983  kbass5  32139  kbass6  32140  dmdmd  32319  atom1d  32372  mdsymlem2  32423  mdsymlem3  32424  mdsymlem4  32425  mdsymlem5  32426  fmptco1f1o  32643  2ndresdju  32659  fnpreimac  32681  fsumiunle  32831  s3f1  32931  swrdf1  32941  dfmgc2lem  32985  dfmgc2  32986  pwrssmgc  32990  mgcf1o  32993  chnso  33004  mndlrinvb  33030  mndlactf1  33031  mndractf1  33033  gsummpt2co  33051  gsumwrd2dccatlem  33069  tocyccntz  33164  cycpmconjs  33176  urpropd  33236  elrgspnlem2  33247  elrgspnlem4  33249  elrgspnsubrunlem2  33252  elrgspnsubrun  33253  erler  33269  rlocaddval  33272  rlocmulval  33273  rlocf1  33277  domnprodn0  33279  rrgsubm  33287  subrdom  33288  isdrng4  33298  suborng  33345  eqgvscpbl  33378  dvdsruasso  33413  nsgmgclem  33439  nsgmgc  33440  nsgqusf1olem2  33442  nsgqusf1olem3  33443  lmhmqusker  33445  intlidl  33448  rhmquskerlem  33453  elrspunidl  33456  elrspunsn  33457  idlinsubrg  33459  rhmimaidl  33460  drngidl  33461  prmidl2  33469  idlmulssprm  33470  isprmidlc  33475  rhmpreimaprmidl  33479  qsidomlem1  33480  qsidomlem2  33481  ssdifidllem  33484  ssdifidlprm  33486  mxidlprm  33498  mxidlirredi  33499  ssmxidllem  33501  opprlidlabs  33513  qsdrngi  33523  rsprprmprmidl  33550  rsprprmprmidlb  33551  rprmirred  33559  rprmirredb  33560  rprmdvdsprod  33562  1arithidom  33565  1arithufdlem3  33574  1arithufdlem4  33575  r1plmhm  33630  r1pquslmic  33631  ply1degltdimlem  33673  ply1degltdim  33674  lindsun  33676  lbsdiflsp0  33677  fedgmullem1  33680  fedgmul  33682  lactlmhm  33685  assalactf1o  33686  extdg1id  33716  fldextrspunlsplem  33723  fldextrspunlsp  33724  minplyirred  33754  algextdeglem8  33765  constrextdg2lem  33789  constrextdg2  33790  zart0  33878  pstmxmet  33896  ordtconnlem1  33923  esumiun  34095  dya2iocnei  34284  omssubadd  34302  actfunsnf1o  34619  fsum2dsub  34622  reprsuc  34630  reprinfz1  34637  reprpmtf1o  34641  breprexplema  34645  circlemeth  34655  hgt750lemb  34671  cusgr3cyclex  35141  resconn  35251  pibt2  37418  uncf  37606  unccur  37610  fin2so  37614  matunitlindflem1  37623  poimirlem6  37633  poimirlem7  37634  poimirlem25  37652  poimirlem28  37655  poimirlem31  37658  poimirlem32  37659  broucube  37661  ismblfin  37668  mbfposadd  37674  itg2gt0cn  37682  ftc1anclem7  37706  ftc1anc  37708  cover2  37722  indexa  37740  filbcmb  37747  seqpo  37754  incsequz  37755  isbnd2  37790  ghomco  37898  unichnidl  38038  isfldidl  38075  dihvalc  41235  dihvalb  41239  uzindd  41978  aks4d1p8  42088  evlselv  42597  fsuppind  42600  radcnvrat  44333  rexabslelem  45429  rexlimddv2  45838  dvnprodlem2  45962  etransclem46  46295  isgrtri  47910  grlimgrtri  47963  lubeldm2  48853  glbeldm2  48854  thincciso2  49104  aacllem  49320