Metamath Proof Explorer

Theorem cgrcom

Description: Congruence commutes between the two sides. (Contributed by Scott Fenton, 12-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 cgrcomim ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrCD→CDCgrAB
2 cgrcomim ⊢N∈ℕ∧C∈𝔼⁡N∧D∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N→CDCgrAB→ABCgrCD
3 2 3com23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→CDCgrAB→ABCgrCD
4 1 3 impbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrCD↔CDCgrAB