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 → A B Cgr C D ↔ B A Cgr D C

Proof

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