Metamath Proof Explorer

Theorem cgrcoml

Description: Congruence commutes on the left. Biconditional version of Theorem 2.4 of Schwabhauser p. 27. (Contributed by Scott Fenton, 12-Jun-2013)

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

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 1 2 3 cgrrflx2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrBA
5 simp3l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→C∈𝔼⁡N
6 simp3r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→D∈𝔼⁡N
7 axcgrtr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrBA∧ABCgrCD→BACgrCD
8 1 2 3 3 2 5 6 7 syl133anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrBA∧ABCgrCD→BACgrCD
9 4 8 mpand ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrCD→BACgrCD
10 1 3 2 cgrrflx2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BACgrAB
11 axcgrtr ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BACgrAB∧BACgrCD→ABCgrCD
12 1 3 2 2 3 5 6 11 syl133anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BACgrAB∧BACgrCD→ABCgrCD
13 10 12 mpand ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BACgrCD→ABCgrCD
14 9 13 impbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrCD↔BACgrCD