Metamath Proof Explorer

Theorem cgr3permute3

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

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

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 cgrcomlr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→ABCgrDE↔BACgrED
5 1 2 3 4 syl3an ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCgrDE↔BACgrED
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 cgrcomlr ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N→ACCgrDF↔CACgrFD
9 1 6 7 8 syl3an ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ACCgrDF↔CACgrFD
10 5 9 3anbi12d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCgrDE∧ACCgrDF∧BCCgrEF↔BACgrED∧CACgrFD∧BCCgrEF
11 3anrot ⊢BCCgrEF∧BACgrED∧CACgrFD↔BACgrED∧CACgrFD∧BCCgrEF
12 10 11 bitr4di ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCgrDE∧ACCgrDF∧BCCgrEF↔BCCgrEF∧BACgrED∧CACgrFD
13 brcgr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF↔ABCgrDE∧ACCgrDF∧BCCgrEF
14 biid ⊢N∈ℕ↔N∈ℕ
15 3anrot ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N↔B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N
16 3anrot ⊢D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N↔E∈𝔼⁡N∧F∈𝔼⁡N∧D∈𝔼⁡N
17 brcgr3 ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧D∈𝔼⁡N→BCACgr3EFD↔BCCgrEF∧BACgrED∧CACgrFD
18 14 15 16 17 syl3anb ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BCACgr3EFD↔BCCgrEF∧BACgrED∧CACgrFD
19 12 13 18 3bitr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF↔BCACgr3EFD