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 208  df-an 397

This theorem is referenced by:  anass  469  anabss3  681  biadanid  828  reximddv3  3156  rspc4v  3580  f1elima  7207  fnfvof  7637  frxp3  8091  oecl  8462  oaass  8486  oen0  8512  oeworde  8519  omabs  8577  oiiniseg  9438  cardinfima  10010  fpwwe2lem11  10555  ltmul12a  12002  eluzp1m1  12805  lbzbi  12877  qreccl  12910  xrlttr  13082  elfzodifsumelfzo  13677  quoremnn0  13806  incexc2  15794  mertens  15842  ndvdsadd  16370  nn0seqcvgd  16530  isprm3  16643  isprm7  16669  pcval  16806  prdsval  17409  evlfcl  18179  chnso  18581  ghmqusnsg  19248  ghmquskerlem3  19252  frgpup1  19741  frgpup3lem  19743  ghmcmn  19797  gsumval3  19873  gsumzoppg  19910  ablfaclem2  20054  gsumdixp  20289  suborng  20848  rhmpreimaidl  21270  rhmqusnsg  21278  frlmgsum  21747  psrass1lem  21908  psrass1  21938  psdmul  22154  evls1maplmhm  22363  m2cpminvid2  22738  pmatcollpw2lem  22760  chcoeffeqlem  22868  neissex  23110  neiptopnei  23115  dissnlocfin  23512  tx1stc  23633  kqreglem1  23724  xpstopnlem1  23792  alexsublem  24027  metuel2  24548  icoopnst  24924  iocopnst  24925  volcn  25591  mbflimsup  25651  mbflim  25653  itg1addlem4  25684  itg1addlem5  25685  itg1climres  25699  limcflf  25866  dvcobr  25931  dvcnvlem  25961  dvfsumge  26007  mdegmullem  26061  plyeq0lem  26193  plypf1  26195  mtestbdd  26388  mbfulm  26389  fsumdvdscom  27166  muinv  27174  logfaclbnd  27203  logexprlim  27206  dchrinv  27242  lgsval3  27296  2sqmo  27418  rpvmasum2  27493  dchrisum0lem1  27497  dchrisum0  27501  selberg  27529  selberg3lem1  27538  selberg34r  27552  pntsval2  27557  nosupbnd1lem5  27694  noinfbnd1lem5  27709  nocvxminlem  27764  oldbday  27911  peano5uzs  28414  iscgrglt  28600  ercgrg  28603  legso  28685  oppperpex  28839  hpgerlem  28851  trgcopyeu  28892  dfcgra2  28916  inaghl  28931  colinearalg  28997  axeuclid  29050  axcontlem2  29052  axcontlem7  29057  wlkiswwlksupgr2  29963  grpoidinvlem4  30596  ipblnfi  30944  shmodsi  31478  eighmorth  32053  kbass5  32209  kbass6  32210  dmdmd  32389  atom1d  32442  mdsymlem2  32493  mdsymlem3  32494  mdsymlem4  32495  mdsymlem5  32496  fmptco1f1o  32725  2ndresdju  32741  fnpreimac  32762  fsumiunle  32921  s3f1  33026  swrdf1  33035  dfmgc2lem  33074  dfmgc2  33075  pwrssmgc  33079  mgcf1o  33082  mndlrinvb  33104  mndlactf1  33105  mndractf1  33107  gsummpt2co  33129  gsumwrd2dccatlem  33158  tocyccntz  33225  cycpmconjs  33237  conjga  33251  fxpsubrg  33255  urpropd  33312  elrgspnlem2  33324  elrgspnlem4  33326  elrgspnsubrunlem2  33329  elrgspnsubrun  33330  erler  33346  rlocaddval  33349  rlocmulval  33350  rlocf1  33354  domnprodn0  33356  domnprodeq0  33357  rrgsubm  33365  subrdom  33366  ricdomn1  33370  isdrng4  33379  eqgvscpbl  33433  dvdsruasso  33468  nsgmgclem  33494  nsgmgc  33495  nsgqusf1olem2  33497  nsgqusf1olem3  33498  lmhmqusker  33500  intlidl  33503  rhmquskerlem  33508  elrspunidl  33511  elrspunsn  33512  idlinsubrg  33514  rhmimaidl  33515  drngidl  33516  prmidl2  33524  idlmulssprm  33525  isprmidlc  33530  rhmpreimaprmidl  33534  qsidomlem1  33535  qsidomlem2  33536  ssdifidllem  33539  ssdifidlprm  33541  mxidlprm  33553  mxidlirredi  33554  ssmxidllem  33556  opprlidlabs  33568  qsdrngi  33578  rsprprmprmidl  33605  rsprprmprmidlb  33606  rprmirred  33614  rprmirredb  33615  rprmdvdsprod  33617  1arithidom  33620  1arithufdlem3  33629  1arithufdlem4  33630  deg1prod  33666  r1plmhm  33693  r1pquslmic  33694  0mplrim  33698  selvply1rhmlema  33702  selvply1rhmlem1  33704  selvply1rhm  33709  mplidomlem  33711  extvfvcl  33720  mplvrpmga  33729  mplvrpmmhm  33730  mplvrpmrhm  33731  psrgsum  33732  psrmonprod  33736  esplyfval1  33757  esplyfvaln  33758  vieta  33764  ply1degltdimlem  33806  ply1degltdim  33807  lindsun  33809  lbsdiflsp0  33810  fedgmullem1  33813  fedgmul  33815  lactlmhm  33818  assalactf1o  33819  extdg1id  33850  fldextrspunlsplem  33857  fldextrspunlsp  33858  extdgfialglem2  33877  extdgfialg  33878  minplyirred  33895  algextdeglem8  33908  constrextdg2lem  33932  constrextdg2  33933  constrfiss  33935  constrsdrg  33959  cos9thpiminplylem2  33967  zart0  34063  pstmxmet  34081  ordtconnlem1  34108  esumiun  34278  dya2iocnei  34466  omssubadd  34484  actfunsnf1o  34788  fsum2dsub  34791  reprsuc  34799  reprinfz1  34806  reprpmtf1o  34810  breprexplema  34814  circlemeth  34824  hgt750lemb  34840  cusgr3cyclex  35364  resconn  35474  pibt2  37779  uncf  37966  unccur  37970  fin2so  37974  matunitlindflem1  37983  poimirlem6  37993  poimirlem7  37994  poimirlem25  38012  poimirlem28  38015  poimirlem31  38018  poimirlem32  38019  broucube  38021  ismblfin  38028  mbfposadd  38034  itg2gt0cn  38042  ftc1anclem7  38066  ftc1anc  38068  cover2  38082  indexa  38100  filbcmb  38107  seqpo  38114  incsequz  38115  isbnd2  38150  ghomco  38258  unichnidl  38398  isfldidl  38435  dihvalc  41725  dihvalb  41729  uzindd  42463  aks4d1p8  42572  evlselv  43039  fsuppind  43040  radcnvrat  44758  rexabslelem  45861  rexlimddv2  46266  dvnprodlem2  46390  etransclem46  46723  isgrtri  48434  grlimgrtri  48494  lubeldm2  49446  glbeldm2  49447  thincciso2  49945  aacllem  50291