Metamath Proof Explorer


Theorem omndmnd

Description: A left-ordered monoid is a monoid. (Contributed by Thierry Arnoux, 13-Mar-2018)

Ref Expression
Assertion omndmnd MoMndMMnd

Proof

Step Hyp Ref Expression
1 eqid BaseM=BaseM
2 eqid +M=+M
3 eqid M=M
4 1 2 3 isomnd MoMndMMndMTosetaBaseMbBaseMcBaseMaMba+McMb+Mc
5 4 simp1bi MoMndMMnd