# 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 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{C},{D}⟩\to ⟨{C},{D}⟩\mathrm{Cgr}⟨{A},{B}⟩\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to {N}\in ℕ$
2 simp2l ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to {A}\in 𝔼\left({N}\right)$
3 simp2r ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to {B}\in 𝔼\left({N}\right)$
4 simp3l ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to {C}\in 𝔼\left({N}\right)$
5 simp3r ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to {D}\in 𝔼\left({N}\right)$
6 simpr ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge ⟨{A},{B}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\to ⟨{A},{B}⟩\mathrm{Cgr}⟨{C},{D}⟩$
7 simpl1 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge ⟨{A},{B}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\to {N}\in ℕ$
8 simpl2l ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge ⟨{A},{B}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\to {A}\in 𝔼\left({N}\right)$
9 simpl2r ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge ⟨{A},{B}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\to {B}\in 𝔼\left({N}\right)$
10 7 8 9 cgrrflxd ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge ⟨{A},{B}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\to ⟨{A},{B}⟩\mathrm{Cgr}⟨{A},{B}⟩$
11 1 2 3 4 5 2 3 6 10 cgrtr4and ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge ⟨{A},{B}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\to ⟨{C},{D}⟩\mathrm{Cgr}⟨{A},{B}⟩$
12 11 ex ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{C},{D}⟩\to ⟨{C},{D}⟩\mathrm{Cgr}⟨{A},{B}⟩\right)$