Metamath Proof Explorer


Syntax definition ccmtN

Description: Extend class notation with the commutes relation.

Ref Expression
Assertion ccmtN class cm