Metamath Proof Explorer


Syntax definition cgcdOLD

Description: Extend class notation to include the gdc function. (New usage is discouraged.)

Ref Expression
Assertion cgcdOLD class gcd OLD A B