a,b,c:
. a
(bc) = (ab)ca,b:. (a ~ b) 
a = ba,b:. (a
b) ~ (ab)BC) ~ ((AB)C)| Rank | Theorem | Name |
| 9 | a,b,c:. a(bc) = (ab)c | [mul_assoc_from_cross_assoc] |
| cites the following: | ||
| 4 | a,b:. (a ~ b) a = b | [fin_card_vs_nat_eq] |
| 8 | a,b:. (ab) ~ (ab) | [nsub_mul_rw] |
| 0 | BC) ~ ((AB)C) | [simple_card_cross_assoc] |