Metamath Proof Explorer

Theorem cgr3permute3

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

		Ref	Expression
	Assertion	cgr3permute3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨D, ⟨E, F⟩⟩ \leftrightarrow ⟨B, ⟨C, A⟩⟩ Cgr3 ⟨E, ⟨F, D⟩⟩)$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ N \in ℕ \to N \in ℕ$
2		3simpa	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (A \in 𝔼 (N) \land B \in 𝔼 (N))$
3		3simpa	$⊢ (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N)) \to (D \in 𝔼 (N) \land E \in 𝔼 (N))$
4		cgrcomlr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨D, E⟩ \leftrightarrow ⟨B, A⟩ Cgr ⟨E, D⟩)$
5	1 2 3 4	syl3an	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨D, E⟩ \leftrightarrow ⟨B, A⟩ Cgr ⟨E, D⟩)$
6		3simpb	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (A \in 𝔼 (N) \land C \in 𝔼 (N))$
7		3simpb	$⊢ (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N)) \to (D \in 𝔼 (N) \land F \in 𝔼 (N))$
8		cgrcomlr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, C⟩ Cgr ⟨D, F⟩ \leftrightarrow ⟨C, A⟩ Cgr ⟨F, D⟩)$
9	1 6 7 8	syl3an	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, C⟩ Cgr ⟨D, F⟩ \leftrightarrow ⟨C, A⟩ Cgr ⟨F, D⟩)$
10	5 9	3anbi12d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to ((⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩) \leftrightarrow (⟨B, A⟩ Cgr ⟨E, D⟩ \land ⟨C, A⟩ Cgr ⟨F, D⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))$
11		3anrot	$⊢ (⟨B, C⟩ Cgr ⟨E, F⟩ \land ⟨B, A⟩ Cgr ⟨E, D⟩ \land ⟨C, A⟩ Cgr ⟨F, D⟩) \leftrightarrow (⟨B, A⟩ Cgr ⟨E, D⟩ \land ⟨C, A⟩ Cgr ⟨F, D⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)$
12	10 11	syl6bbr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to ((⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩) \leftrightarrow (⟨B, C⟩ Cgr ⟨E, F⟩ \land ⟨B, A⟩ Cgr ⟨E, D⟩ \land ⟨C, A⟩ Cgr ⟨F, D⟩))$
13		brcgr3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨D, ⟨E, F⟩⟩ \leftrightarrow (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))$
14		biid	$⊢ N \in ℕ \leftrightarrow N \in ℕ$
15		3anrot	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \leftrightarrow (B \in 𝔼 (N) \land C \in 𝔼 (N) \land A \in 𝔼 (N))$
16		3anrot	$⊢ (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N)) \leftrightarrow (E \in 𝔼 (N) \land F \in 𝔼 (N) \land D \in 𝔼 (N))$
17		brcgr3	$⊢ (N \in ℕ \land (B \in 𝔼 (N) \land C \in 𝔼 (N) \land A \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨B, ⟨C, A⟩⟩ Cgr3 ⟨E, ⟨F, D⟩⟩ \leftrightarrow (⟨B, C⟩ Cgr ⟨E, F⟩ \land ⟨B, A⟩ Cgr ⟨E, D⟩ \land ⟨C, A⟩ Cgr ⟨F, D⟩))$
18	14 15 16 17	syl3anb	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨B, ⟨C, A⟩⟩ Cgr3 ⟨E, ⟨F, D⟩⟩ \leftrightarrow (⟨B, C⟩ Cgr ⟨E, F⟩ \land ⟨B, A⟩ Cgr ⟨E, D⟩ \land ⟨C, A⟩ Cgr ⟨F, D⟩))$
19	12 13 18	3bitr4d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨D, ⟨E, F⟩⟩ \leftrightarrow ⟨B, ⟨C, A⟩⟩ Cgr3 ⟨E, ⟨F, D⟩⟩)$