Metamath Proof Explorer

Theorem cgrcomim

Description: Congruence commutes on the two sides. Implication version. Theorem 2.2 of Schwabhauser p. 27. (Contributed by Scott Fenton, 12-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→N∈ℕ
2 simp2l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→A∈𝔼⁡N
3 simp2r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→B∈𝔼⁡N
4 simp3l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→C∈𝔼⁡N
5 simp3r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→D∈𝔼⁡N
6 simpr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧ABCgrCD→ABCgrCD
7 simpl1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧ABCgrCD→N∈ℕ
8 simpl2l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧ABCgrCD→A∈𝔼⁡N
9 simpl2r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧ABCgrCD→B∈𝔼⁡N
10 7 8 9 cgrrflxd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧ABCgrCD→ABCgrAB
11 1 2 3 4 5 2 3 6 10 cgrtr4and ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧ABCgrCD→CDCgrAB
12 11 ex ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrCD→CDCgrAB