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  3593  f1elima  7206  fnfvof  7636  frxp3  8090  oecl  8461  oaass  8485  oen0  8510  oeworde  8517  omabs  8575  oiiniseg  9430  cardinfima  9999  fpwwe2lem11  10543  ltmul12a  11988  eluzp1m1  12768  lbzbi  12840  qreccl  12873  xrlttr  13045  elfzodifsumelfzo  13638  quoremnn0  13767  incexc2  15752  mertens  15800  ndvdsadd  16328  nn0seqcvgd  16488  isprm3  16601  isprm7  16626  pcval  16763  prdsval  17366  evlfcl  18136  chnso  18538  ghmqusnsg  19202  ghmquskerlem3  19206  frgpup1  19695  frgpup3lem  19697  ghmcmn  19751  gsumval3  19827  gsumzoppg  19864  ablfaclem2  20008  gsumdixp  20245  suborng  20800  rhmpreimaidl  21223  rhmqusnsg  21231  frlmgsum  21718  psrass1lem  21879  psrass1  21910  psdmul  22100  evls1maplmhm  22312  m2cpminvid2  22690  pmatcollpw2lem  22712  chcoeffeqlem  22820  neissex  23062  neiptopnei  23067  dissnlocfin  23464  tx1stc  23585  kqreglem1  23676  xpstopnlem1  23744  alexsublem  23979  metuel2  24500  icoopnst  24883  iocopnst  24884  volcn  25554  mbflimsup  25614  mbflim  25616  itg1addlem4  25647  itg1addlem5  25648  itg1climres  25662  limcflf  25829  dvcobr  25896  dvcobrOLD  25897  dvcnvlem  25927  dvfsumge  25975  mdegmullem  26030  plyeq0lem  26162  plypf1  26164  mtestbdd  26361  mbfulm  26362  fsumdvdscom  27142  muinv  27150  logfaclbnd  27180  logexprlim  27183  dchrinv  27219  lgsval3  27273  2sqmo  27395  rpvmasum2  27470  dchrisum0lem1  27474  dchrisum0  27478  selberg  27506  selberg3lem1  27515  selberg34r  27529  pntsval2  27534  nosupbnd1lem5  27671  noinfbnd1lem5  27686  nocvxminlem  27737  oldbday  27866  peano5uzs  28348  iscgrglt  28512  ercgrg  28515  legso  28597  oppperpex  28751  hpgerlem  28763  trgcopyeu  28804  dfcgra2  28828  inaghl  28843  colinearalg  28909  axeuclid  28962  axcontlem2  28964  axcontlem7  28969  wlkiswwlksupgr2  29876  grpoidinvlem4  30508  ipblnfi  30856  shmodsi  31390  eighmorth  31965  kbass5  32121  kbass6  32122  dmdmd  32301  atom1d  32354  mdsymlem2  32405  mdsymlem3  32406  mdsymlem4  32407  mdsymlem5  32408  fmptco1f1o  32637  2ndresdju  32653  fnpreimac  32675  fsumiunle  32838  s3f1  32957  swrdf1  32966  dfmgc2lem  33005  dfmgc2  33006  pwrssmgc  33010  mgcf1o  33013  mndlrinvb  33035  mndlactf1  33036  mndractf1  33038  gsummpt2co  33059  gsumwrd2dccatlem  33087  tocyccntz  33154  cycpmconjs  33166  conjga  33180  fxpsubrg  33184  urpropd  33241  elrgspnlem2  33253  elrgspnlem4  33255  elrgspnsubrunlem2  33258  elrgspnsubrun  33259  erler  33275  rlocaddval  33278  rlocmulval  33279  rlocf1  33283  domnprodn0  33285  domnprodeq0  33286  rrgsubm  33294  subrdom  33295  isdrng4  33305  eqgvscpbl  33359  dvdsruasso  33394  nsgmgclem  33420  nsgmgc  33421  nsgqusf1olem2  33423  nsgqusf1olem3  33424  lmhmqusker  33426  intlidl  33429  rhmquskerlem  33434  elrspunidl  33437  elrspunsn  33438  idlinsubrg  33440  rhmimaidl  33441  drngidl  33442  prmidl2  33450  idlmulssprm  33451  isprmidlc  33456  rhmpreimaprmidl  33460  qsidomlem1  33461  qsidomlem2  33462  ssdifidllem  33465  ssdifidlprm  33467  mxidlprm  33479  mxidlirredi  33480  ssmxidllem  33482  opprlidlabs  33494  qsdrngi  33504  rsprprmprmidl  33531  rsprprmprmidlb  33532  rprmirred  33540  rprmirredb  33541  rprmdvdsprod  33543  1arithidom  33546  1arithufdlem3  33555  1arithufdlem4  33556  deg1prod  33592  r1plmhm  33619  r1pquslmic  33620  extvfvcl  33629  mplvrpmga  33638  mplvrpmmhm  33639  mplvrpmrhm  33640  vieta  33664  ply1degltdimlem  33707  ply1degltdim  33708  lindsun  33710  lbsdiflsp0  33711  fedgmullem1  33714  fedgmul  33716  lactlmhm  33719  assalactf1o  33720  extdg1id  33751  fldextrspunlsplem  33758  fldextrspunlsp  33759  extdgfialglem2  33778  extdgfialg  33779  minplyirred  33796  algextdeglem8  33809  constrextdg2lem  33833  constrextdg2  33834  constrfiss  33836  constrsdrg  33860  cos9thpiminplylem2  33868  zart0  33964  pstmxmet  33982  ordtconnlem1  34009  esumiun  34179  dya2iocnei  34367  omssubadd  34385  actfunsnf1o  34689  fsum2dsub  34692  reprsuc  34700  reprinfz1  34707  reprpmtf1o  34711  breprexplema  34715  circlemeth  34725  hgt750lemb  34741  cusgr3cyclex  35252  resconn  35362  pibt2  37534  uncf  37712  unccur  37716  fin2so  37720  matunitlindflem1  37729  poimirlem6  37739  poimirlem7  37740  poimirlem25  37758  poimirlem28  37761  poimirlem31  37764  poimirlem32  37765  broucube  37767  ismblfin  37774  mbfposadd  37780  itg2gt0cn  37788  ftc1anclem7  37812  ftc1anc  37814  cover2  37828  indexa  37846  filbcmb  37853  seqpo  37860  incsequz  37861  isbnd2  37896  ghomco  38004  unichnidl  38144  isfldidl  38181  dihvalc  41405  dihvalb  41409  uzindd  42143  aks4d1p8  42253  evlselv  42745  fsuppind  42748  radcnvrat  44471  rexabslelem  45578  rexlimddv2  45983  dvnprodlem2  46107  etransclem46  46440  isgrtri  48105  grlimgrtri  48165  lubeldm2  49117  glbeldm2  49118  thincciso2  49616  aacllem  49962