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

Proof

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