Metamath Proof Explorer

Theorem cgr3com

Description: Commutativity law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion cgr3com ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF↔DEFCgr3ABC

Proof

Step Hyp Ref Expression
1 id ⊢N∈ℕ→N∈ℕ
2 3simpa ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→A∈𝔼⁡N∧B∈𝔼⁡N
3 3simpa ⊢D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→D∈𝔼⁡N∧E∈𝔼⁡N
4 cgrcom ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→ABCgrDE↔DECgrAB
5 1 2 3 4 syl3an ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCgrDE↔DECgrAB
6 3simpb ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→A∈𝔼⁡N∧C∈𝔼⁡N
7 3simpb ⊢D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→D∈𝔼⁡N∧F∈𝔼⁡N
8 cgrcom ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N→ACCgrDF↔DFCgrAC
9 1 6 7 8 syl3an ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ACCgrDF↔DFCgrAC
10 3simpc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B∈𝔼⁡N∧C∈𝔼⁡N
11 3simpc ⊢D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→E∈𝔼⁡N∧F∈𝔼⁡N
12 cgrcom ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BCCgrEF↔EFCgrBC
13 1 10 11 12 syl3an ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BCCgrEF↔EFCgrBC
14 5 9 13 3anbi123d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCgrDE∧ACCgrDF∧BCCgrEF↔DECgrAB∧DFCgrAC∧EFCgrBC
15 brcgr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF↔ABCgrDE∧ACCgrDF∧BCCgrEF
16 brcgr3 ⊢N∈ℕ∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→DEFCgr3ABC↔DECgrAB∧DFCgrAC∧EFCgrBC
17 16 3com23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→DEFCgr3ABC↔DECgrAB∧DFCgrAC∧EFCgrBC
18 14 15 17 3bitr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF↔DEFCgr3ABC