Metamath Proof Explorer

Theorem cgr3permute2

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

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

Proof

Step Hyp Ref Expression
1 cgr3permute3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF↔BCACgr3EFD
2 biid ⊢N∈ℕ↔N∈ℕ
3 3anrot ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N↔B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N
4 3anrot ⊢D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N↔E∈𝔼⁡N∧F∈𝔼⁡N∧D∈𝔼⁡N
5 cgr3permute1 ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧D∈𝔼⁡N→BCACgr3EFD↔BACCgr3EDF
6 2 3 4 5 syl3anb ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BCACgr3EFD↔BACCgr3EDF
7 1 6 bitrd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF↔BACCgr3EDF