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  1381  reximddv3  3183  rspc4v  3599  coass  6290  f1elima  7298  fnfvof  7742  frxp3  8205  oecl  8583  oaass  8607  oen0  8633  oeworde  8640  omabs  8698  uncf  8929  oiiniseg  9564  cardinfima  10215  fpwwe2lem11  10765  ltmul12a  12213  eluzp1m1  13031  lbzbi  13103  qreccl  13137  xrlttr  13309  elfzodifsumelfzo  13906  quoremnn0  14036  swrdf1  14841  incexc2  16051  mertens  16099  ndvdsadd  16624  nn0seqcvgd  16789  isprm3  16902  isprm7  16928  pcval  17066  prdsval  17676  evlfcl  18446  chnso  18848  ghmqusnsg  19547  ghmquskerlem3  19551  frgpup1  20040  frgpup3lem  20042  ghmcmn  20096  gsumval3  20172  gsumzoppg  20209  ablfaclem2  20353  gsumdixp  20599  isdrng4  21043  suborng  21184  drngidl  21590  rhmpreimaidl  21622  rhmqusnsg  21632  prmidl2  21673  idlmulssprm  21674  isprmidlc  21679  rhmpreimaprmidl  21686  qsidomlem1  21687  qsidomlem2  21688  ssdifidllem  21691  ssdifidlprm  21693  prmidlsubm  21694  frlmgsum  22133  psrass1lem  22296  psrass1  22326  psdmul  22542  evls1maplmhm  22750  matunitlindflem1  23049  m2cpminvid2  23128  pmatcollpw2lem  23150  chcoeffeqlem  23258  neissex  23500  neiptopnei  23505  dissnlocfin  23903  tx1stc  24024  kqreglem1  24115  xpstopnlem1  24183  alexsublem  24418  metuel2  24939  icoopnst  25315  iocopnst  25316  volcn  25982  mbflimsup  26042  mbflim  26044  itg1addlem4  26075  itg1addlem5  26076  itg1climres  26090  limcflf  26256  dvcobr  26321  dvcnvlem  26351  dvfsumge  26397  mdegmullem  26451  plyeq0lem  26584  plypf1  26586  mtestbdd  26789  mbfulm  26790  fsumdvdscom  27569  muinv  27577  logfaclbnd  27606  logexprlim  27609  dchrinv  27645  lgsval3  27699  2sqmo  27821  rpvmasum2  27896  dchrisum0lem1  27900  dchrisum0  27904  selberg  27932  selberg3lem1  27941  selberg34r  27955  pntsval2  27960  nosupbnd1lem5  28126  noinfbnd1lem5  28141  nocvxminlem  28197  oldbday  28344  peano5uzs  28847  tgsegconeu  29006  iscgrglt  29034  ercgrg  29037  legso  29119  tglinesseq  29165  tglnpt3  29179  tglnpt4  29180  oppperpex  29286  hpgerlem  29300  isplng  29313  plngrotlem3  29324  plng3p  29332  trgcopyeu  29370  zerocgra  29388  dfcgra2  29395  ragcgra  29400  tgaaddcpbllem1  29406  tgaaddcpbl  29409  inaghl  29421  cgraer  29434  angmgmaddeu1  29436  angmgmaddeu2  29437  angmgmaddeu3  29438  angmgmaddeu4  29439  angmgmaddeu5  29440  angmgmaddeu6  29441  angmgmaddeu7  29442  angmgmaddov2lem  29444  angmgmaddov1  29445  angmgmaddov2  29446  angmgmaddcpbl  29447  angmgmaddcl  29448  angmgmaddlid  29449  angmgmaddrid  29450  prlnghpg  29481  dfprlng2  29482  dfprlng3  29483  prlngex  29486  prlngmolem1  29487  prlngmolem2  29488  quadcgrprlng  29501  colinearalg  29545  axeuclid  29598  axcontlem2  29600  axcontlem7  29605  wlkiswwlksupgr2  30523  grpoidinvlem4  31166  ipblnfi  31514  shmodsi  32048  eighmorth  32623  kbass5  32779  kbass6  32780  dmdmd  32959  atom1d  33012  mdsymlem2  33063  mdsymlem3  33064  mdsymlem4  33065  mdsymlem5  33066  fmptco1f1o  33325  2ndresdju  33341  fnpreimac  33362  fsumiunle  33516  s3f1  33607  weinflb  33637  dfmgc2lem  33655  dfmgc2  33656  pwrssmgc  33660  mgcf1o  33663  mndlrinvb  33685  mndlactf1  33686  mndractf1  33688  gsummpt2co  33708  gsumwrd2dccatlem  33737  tocyccntz  33804  cycpmconjs  33816  conjga  33830  fxpsubrg  33834  urpropd  33890  elrgspnlem2  33903  elrgspnlem4  33905  elrgspnsubrunlem2  33908  elrgspnsubrun  33909  erler  33925  rlocaddval  33929  rlocmulval  33930  rlocf1  33934  domnprodn0  33938  domnprodeq0  33939  rrgsubm  33944  subrdom  33945  ricdomn1  33949  edomediv  33955  fldedom  33956  ply1edom  33959  edompidlem  33960  eqgvscpbl  34015  dvdsruasso  34044  nsgmgclem  34066  nsgmgc  34067  nsgqusf1olem2  34069  nsgqusf1olem3  34070  lmhmqusker  34072  intlidl  34074  rhmquskerlem  34079  elrspunidl  34082  elrspunsn  34083  idlinsubrg  34085  rhmimaidl  34086  mxidlprm  34099  mxidlirredi  34100  ssmxidllem  34102  opprlidlabs  34113  qsdrngi  34123  drnglring  34128  dflringlem2  34131  rsprprmprmidl  34158  rsprprmprmidlb  34159  rprmirred  34167  rprmirredb  34168  rprmdvdsprod  34170  1arithidom  34173  1arithufdlem3  34182  1arithufdlem4  34183  deg1prod  34218  r1plmhm  34246  r1pquslmic  34247  0mplrim  34257  selvply1rhmlema  34261  selvply1rhmlem1  34263  selvply1rhm  34268  mplidomlem  34270  extvfvcl  34279  mplvrpmga  34288  mplvrpmmhm  34289  mplvrpmrhm  34290  psrgsum  34291  psrmonprod  34295  esplyfval1  34316  esplyfvaln  34317  vieta  34323  ply1degltdimlem  34365  ply1degltdim  34366  lindsun  34368  lbsdiflsp0  34369  fedgmullem1  34372  fedgmul  34374  lactlmhm  34377  assalactf1o  34378  extdg1id  34409  fldextrspunlsplem  34416  fldextrspunlsp  34417  extdgfialglem2  34436  extdgfialg  34437  minplyirred  34454  algextdeglem8  34467  constrextdg2lem  34491  constrextdg2  34492  constrfiss  34494  constrsdrg  34518  cos9thpiminplylem2  34526  zart0  34622  pstmxmet  34640  ordtconnlem1  34667  esumiun  34837  dya2iocnei  35025  omssubadd  35043  actfunsnf1o  35344  fsum2dsub  35347  reprsuc  35355  reprinfz1  35362  reprpmtf1o  35366  breprexplema  35370  circlemeth  35380  hgt750lemb  35396  cusgr3cyclex  36109  resconn  36219  pibt2  38608  unccur  38794  fin2so  38798  poimirlem6  38812  poimirlem7  38813  poimirlem25  38831  poimirlem28  38834  poimirlem31  38837  poimirlem32  38838  broucube  38840  ismblfin  38847  mbfposadd  38853  itg2gt0cn  38861  ftc1anclem7  38885  ftc1anc  38887  cover2  38917  indexa  38935  filbcmb  38940  seqpo  38947  incsequz  38948  isbnd2  38983  ghomco  39091  unichnidl  39231  isfldidl  39268  dihvalc  42556  dihvalb  42560  uzindd  43294  aks4d1p8  43403  evlselv  43883  fsuppind  43884  radcnvrat  45559  rexabslelem  46701  rexlimddv2  47106  dvnprodlem2  47230  etransclem46  47563  isgrtri  49314  grlimgrtri  49374  prelrrx2bd  50157  lubeldm2  50401  glbeldm2  50402  thincciso2  50921  aacllem  51367