Metamath Proof Explorer

Theorem cgrcomlr

Description: Congruence commutes on both sides. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion cgrcomlr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrCD↔BACgrDC

Proof

Step Hyp Ref Expression
1 cgrcoml ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrCD↔BACgrCD
2 ancom ⊢A∈𝔼⁡N∧B∈𝔼⁡N↔B∈𝔼⁡N∧A∈𝔼⁡N
3 cgrcomr ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BACgrCD↔BACgrDC
4 2 3 syl3an2b ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BACgrCD↔BACgrDC
5 1 4 bitrd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrCD↔BACgrDC