Metamath Proof Explorer


Theorem orngogrp

Description: An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018)

Ref Expression
Assertion orngogrp R oRing R oGrp

Proof

Step Hyp Ref Expression
1 eqid Base R = Base R
2 eqid 0 R = 0 R
3 eqid R = R
4 eqid R = R
5 1 2 3 4 isorng R oRing R Ring R oGrp a Base R b Base R 0 R R a 0 R R b 0 R R a R b
6 5 simp2bi R oRing R oGrp