Theorem addass 9600

Description: Alias for ax-addass 9578, for naming consistency with addassi 9625. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
addass

Proof of Theorem addass

Step	Hyp	Ref	Expression
1		ax-addass 9578	1

Syntax hints:  ->wi 4  /\w3a 973  =wceq 1395  e.wcel 1818  (class class class)co 6296  cc 9511  caddc 9516

This theorem is referenced by:  addassi  9625  addassd  9639  00id  9776  addid2  9784  add12  9814  add32  9815  add32r  9816  add4  9817  nnaddcl  10583  uzaddcl  11166  xaddass  11470  fztp  11765  seradd  12149  expadd  12208  bernneq  12292  faclbnd6  12377  hashgadd  12445  swrds2  12883  clim2ser  13477  clim2ser2  13478  summolem3  13536  isumsplit  13652  odd2np1lem  14045  prmlem0  14591  cnaddablx  16874  cnaddabl  16875  zaddablx  16876  cncrng  18439  pjthlem1  21852  ptolemy  22889  bcp1ctr  23554  wlkdvspthlem  24609  gxnn0add  25276  cnaddablo  25352  pjhthlem1  26309  fsumcube  29822  mblfinlem2  30052  nnsgrp  32505  2zrngasgrp  32746

This theorem was proved from axioms:  ax-addass 9578