Theorem anasss 472

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 425	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 424	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anass  474  anabss3  688  biadanid  835  3anasss  1380  reximddv3  3179  rspc4v  3595  f1elima  7268  fnfvof  7711  frxp3  8171  oecl  8549  oaass  8573  oen0  8599  oeworde  8606  omabs  8664  uncf  8895  oiiniseg  9531  cardinfima  10180  fpwwe2lem11  10730  ltmul12a  12177  eluzp1m1  12995  lbzbi  13067  qreccl  13101  xrlttr  13273  elfzodifsumelfzo  13870  quoremnn0  14000  swrdf1  14804  incexc2  16013  mertens  16061  ndvdsadd  16586  nn0seqcvgd  16751  isprm3  16864  isprm7  16890  pcval  17028  prdsval  17632  evlfcl  18402  chnso  18804  ghmqusnsg  19502  ghmquskerlem3  19506  frgpup1  19995  frgpup3lem  19997  ghmcmn  20051  gsumval3  20127  gsumzoppg  20164  ablfaclem2  20308  gsumdixp  20554  isdrng4  20998  suborng  21139  drngidl  21545  rhmpreimaidl  21577  rhmqusnsg  21587  prmidl2  21628  idlmulssprm  21629  isprmidlc  21634  rhmpreimaprmidl  21641  qsidomlem1  21642  qsidomlem2  21643  ssdifidllem  21646  ssdifidlprm  21648  prmidlsubm  21649  frlmgsum  22084  psrass1lem  22247  psrass1  22277  psdmul  22493  evls1maplmhm  22701  matunitlindflem1  23000  m2cpminvid2  23079  pmatcollpw2lem  23101  chcoeffeqlem  23209  neissex  23451  neiptopnei  23456  dissnlocfin  23854  tx1stc  23975  kqreglem1  24066  xpstopnlem1  24134  alexsublem  24369  metuel2  24890  icoopnst  25266  iocopnst  25267  volcn  25933  mbflimsup  25993  mbflim  25995  itg1addlem4  26026  itg1addlem5  26027  itg1climres  26041  limcflf  26207  dvcobr  26272  dvcnvlem  26302  dvfsumge  26348  mdegmullem  26402  plyeq0lem  26535  plypf1  26537  mtestbdd  26738  mbfulm  26739  fsumdvdscom  27518  muinv  27526  logfaclbnd  27555  logexprlim  27558  dchrinv  27594  lgsval3  27648  2sqmo  27770  rpvmasum2  27845  dchrisum0lem1  27849  dchrisum0  27853  selberg  27881  selberg3lem1  27890  selberg34r  27904  pntsval2  27909  nosupbnd1lem5  28075  noinfbnd1lem5  28090  nocvxminlem  28146  oldbday  28293  peano5uzs  28796  tgsegconeu  28955  iscgrglt  28983  ercgrg  28986  legso  29068  tglinesseq  29114  tglnpt3  29128  tglnpt4  29129  oppperpex  29235  hpgerlem  29249  isplng  29262  plngrotlem3  29273  plng3p  29281  trgcopyeu  29319  zerocgra  29337  dfcgra2  29344  ragcgra  29349  tgaaddcpbllem1  29355  tgaaddcpbl  29358  inaghl  29370  cgraer  29383  angmgmaddeu1  29385  angmgmaddeu2  29386  angmgmaddeu3  29387  angmgmaddeu4  29388  angmgmaddeu5  29389  angmgmaddeu6  29390  angmgmaddeu7  29391  angmgmaddov2lem  29393  angmgmaddov1  29394  angmgmaddov2  29395  angmgmaddcpbl  29396  angmgmaddcl  29397  angmgmaddlid  29398  angmgmaddrid  29399  prlnghpg  29430  dfprlng2  29431  dfprlng3  29432  prlngex  29435  prlngmolem1  29436  prlngmolem2  29437  quadcgrprlng  29450  colinearalg  29494  axeuclid  29547  axcontlem2  29549  axcontlem7  29554  wlkiswwlksupgr2  30472  grpoidinvlem4  31115  ipblnfi  31463  shmodsi  31997  eighmorth  32572  kbass5  32728  kbass6  32729  dmdmd  32908  atom1d  32961  mdsymlem2  33012  mdsymlem3  33013  mdsymlem4  33014  mdsymlem5  33015  fmptco1f1o  33275  2ndresdju  33291  fnpreimac  33312  fsumiunle  33467  s3f1  33558  dfmgc2lem  33603  dfmgc2  33604  pwrssmgc  33608  mgcf1o  33611  mndlrinvb  33633  mndlactf1  33634  mndractf1  33636  gsummpt2co  33656  gsumwrd2dccatlem  33685  tocyccntz  33752  cycpmconjs  33764  conjga  33778  fxpsubrg  33782  urpropd  33838  elrgspnlem2  33851  elrgspnlem4  33853  elrgspnsubrunlem2  33856  elrgspnsubrun  33857  erler  33873  rlocaddval  33877  rlocmulval  33878  rlocf1  33882  domnprodn0  33886  domnprodeq0  33887  rrgsubm  33892  subrdom  33893  ricdomn1  33897  eqgvscpbl  33958  dvdsruasso  33987  nsgmgclem  34009  nsgmgc  34010  nsgqusf1olem2  34012  nsgqusf1olem3  34013  lmhmqusker  34015  intlidl  34017  rhmquskerlem  34022  elrspunidl  34025  elrspunsn  34026  idlinsubrg  34028  rhmimaidl  34029  mxidlprm  34042  mxidlirredi  34043  ssmxidllem  34045  opprlidlabs  34056  qsdrngi  34066  drnglring  34071  dflringlem2  34074  rsprprmprmidl  34101  rsprprmprmidlb  34102  rprmirred  34110  rprmirredb  34111  rprmdvdsprod  34113  1arithidom  34116  1arithufdlem3  34125  1arithufdlem4  34126  deg1prod  34162  r1plmhm  34188  r1pquslmic  34189  0mplrim  34193  selvply1rhmlema  34197  selvply1rhmlem1  34199  selvply1rhm  34204  mplidomlem  34206  extvfvcl  34215  mplvrpmga  34224  mplvrpmmhm  34225  mplvrpmrhm  34226  psrgsum  34227  psrmonprod  34231  esplyfval1  34252  esplyfvaln  34253  vieta  34259  ply1degltdimlem  34301  ply1degltdim  34302  lindsun  34304  lbsdiflsp0  34305  fedgmullem1  34308  fedgmul  34310  lactlmhm  34313  assalactf1o  34314  extdg1id  34345  fldextrspunlsplem  34352  fldextrspunlsp  34353  extdgfialglem2  34372  extdgfialg  34373  minplyirred  34390  algextdeglem8  34403  constrextdg2lem  34427  constrextdg2  34428  constrfiss  34430  constrsdrg  34454  cos9thpiminplylem2  34462  zart0  34558  pstmxmet  34576  ordtconnlem1  34603  esumiun  34773  dya2iocnei  34961  omssubadd  34979  actfunsnf1o  35280  fsum2dsub  35283  reprsuc  35291  reprinfz1  35298  reprpmtf1o  35302  breprexplema  35306  circlemeth  35316  hgt750lemb  35332  cusgr3cyclex  35988  resconn  36098  pibt2  38434  unccur  38620  fin2so  38624  poimirlem6  38638  poimirlem7  38639  poimirlem25  38657  poimirlem28  38660  poimirlem31  38663  poimirlem32  38664  broucube  38666  ismblfin  38673  mbfposadd  38679  itg2gt0cn  38687  ftc1anclem7  38711  ftc1anc  38713  cover2  38743  indexa  38761  filbcmb  38768  seqpo  38775  incsequz  38776  isbnd2  38811  ghomco  38919  unichnidl  39059  isfldidl  39096  dihvalc  42384  dihvalb  42388  uzindd  43122  aks4d1p8  43231  evlselv  43711  fsuppind  43712  radcnvrat  45392  rexabslelem  46522  rexlimddv2  46927  dvnprodlem2  47051  etransclem46  47384  isgrtri  49135  grlimgrtri  49195  prelrrx2bd  49920  lubeldm2  50164  glbeldm2  50165  thincciso2  50684  aacllem  51108