Metamath Proof Explorer

Theorem cgr3permute1

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

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

Proof

Step Hyp Ref Expression
1 id ⊢N∈ℕ→N∈ℕ
2 3simpc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B∈𝔼⁡N∧C∈𝔼⁡N
3 3simpc ⊢D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→E∈𝔼⁡N∧F∈𝔼⁡N
4 cgrcomlr ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BCCgrEF↔CBCgrFE
5 1 2 3 4 syl3an ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BCCgrEF↔CBCgrFE
6 5 3anbi3d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCgrDE∧ACCgrDF∧BCCgrEF↔ABCgrDE∧ACCgrDF∧CBCgrFE
7 3ancoma ⊢ABCgrDE∧ACCgrDF∧CBCgrFE↔ACCgrDF∧ABCgrDE∧CBCgrFE
8 6 7 bitrdi ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCgrDE∧ACCgrDF∧BCCgrEF↔ACCgrDF∧ABCgrDE∧CBCgrFE
9 brcgr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF↔ABCgrDE∧ACCgrDF∧BCCgrEF
10 biid ⊢N∈ℕ↔N∈ℕ
11 3ancomb ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N↔A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N
12 3ancomb ⊢D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N↔D∈𝔼⁡N∧F∈𝔼⁡N∧E∈𝔼⁡N
13 brcgr3 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧E∈𝔼⁡N→ACBCgr3DFE↔ACCgrDF∧ABCgrDE∧CBCgrFE
14 10 11 12 13 syl3anb ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ACBCgr3DFE↔ACCgrDF∧ABCgrDE∧CBCgrFE
15 8 9 14 3bitr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF↔ACBCgr3DFE