cgr3tr4

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

		Ref	Expression
	Assertion	cgr3tr4	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to ((⟨A, ⟨B, C⟩⟩ Cgr3 ⟨D, ⟨E, F⟩⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨G, ⟨H, I⟩⟩) \to ⟨D, ⟨E, F⟩⟩ Cgr3 ⟨G, ⟨H, I⟩⟩)$

Proof

Step	Hyp	Ref	Expression
1		3an6	$⊢ ((⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, B⟩ Cgr ⟨G, H⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨A, C⟩ Cgr ⟨G, I⟩) \land (⟨B, C⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨H, I⟩)) \leftrightarrow ((⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩) \land (⟨A, B⟩ Cgr ⟨G, H⟩ \land ⟨A, C⟩ Cgr ⟨G, I⟩ \land ⟨B, C⟩ Cgr ⟨H, I⟩))$
2		simpl	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to N \in ℕ$
3		simpr11	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to A \in 𝔼 (N)$
4		simpr12	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to B \in 𝔼 (N)$
5		simpr21	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to D \in 𝔼 (N)$
6		simpr22	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to E \in 𝔼 (N)$
7		simpr31	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to G \in 𝔼 (N)$
8		simpr32	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to H \in 𝔼 (N)$
9		axcgrtr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land D \in 𝔼 (N)) \land (E \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, B⟩ Cgr ⟨G, H⟩) \to ⟨D, E⟩ Cgr ⟨G, H⟩)$
10	2 3 4 5 6 7 8 9	syl133anc	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to ((⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, B⟩ Cgr ⟨G, H⟩) \to ⟨D, E⟩ Cgr ⟨G, H⟩)$
11		simpr13	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to C \in 𝔼 (N)$
12		simpr23	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to F \in 𝔼 (N)$
13		simpr33	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to I \in 𝔼 (N)$
14		axcgrtr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land I \in 𝔼 (N))) \to ((⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨A, C⟩ Cgr ⟨G, I⟩) \to ⟨D, F⟩ Cgr ⟨G, I⟩)$
15	2 3 11 5 12 7 13 14	syl133anc	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to ((⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨A, C⟩ Cgr ⟨G, I⟩) \to ⟨D, F⟩ Cgr ⟨G, I⟩)$
16		axcgrtr	$⊢ (N \in ℕ \land (B \in 𝔼 (N) \land C \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N))) \to ((⟨B, C⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨H, I⟩) \to ⟨E, F⟩ Cgr ⟨H, I⟩)$
17	2 4 11 6 12 8 13 16	syl133anc	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to ((⟨B, C⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨H, I⟩) \to ⟨E, F⟩ Cgr ⟨H, I⟩)$
18	10 15 17	3anim123d	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to (((⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, B⟩ Cgr ⟨G, H⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨A, C⟩ Cgr ⟨G, I⟩) \land (⟨B, C⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨H, I⟩)) \to (⟨D, E⟩ Cgr ⟨G, H⟩ \land ⟨D, F⟩ Cgr ⟨G, I⟩ \land ⟨E, F⟩ Cgr ⟨H, I⟩))$
19	1 18	biimtrrid	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to (((⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩) \land (⟨A, B⟩ Cgr ⟨G, H⟩ \land ⟨A, C⟩ Cgr ⟨G, I⟩ \land ⟨B, C⟩ Cgr ⟨H, I⟩)) \to (⟨D, E⟩ Cgr ⟨G, H⟩ \land ⟨D, F⟩ Cgr ⟨G, I⟩ \land ⟨E, F⟩ Cgr ⟨H, I⟩))$
20		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⟩))$
21	20	3adant3r3	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \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⟩))$
22		brcgr3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N))) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨G, ⟨H, I⟩⟩ \leftrightarrow (⟨A, B⟩ Cgr ⟨G, H⟩ \land ⟨A, C⟩ Cgr ⟨G, I⟩ \land ⟨B, C⟩ Cgr ⟨H, I⟩))$
23	22	3adant3r2	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨G, ⟨H, I⟩⟩ \leftrightarrow (⟨A, B⟩ Cgr ⟨G, H⟩ \land ⟨A, C⟩ Cgr ⟨G, I⟩ \land ⟨B, C⟩ Cgr ⟨H, I⟩))$
24	21 23	anbi12d	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to ((⟨A, ⟨B, C⟩⟩ Cgr3 ⟨D, ⟨E, F⟩⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨G, ⟨H, I⟩⟩) \leftrightarrow ((⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩) \land (⟨A, B⟩ Cgr ⟨G, H⟩ \land ⟨A, C⟩ Cgr ⟨G, I⟩ \land ⟨B, C⟩ Cgr ⟨H, I⟩)))$
25		brcgr3	$⊢ (N \in ℕ \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N))) \to (⟨D, ⟨E, F⟩⟩ Cgr3 ⟨G, ⟨H, I⟩⟩ \leftrightarrow (⟨D, E⟩ Cgr ⟨G, H⟩ \land ⟨D, F⟩ Cgr ⟨G, I⟩ \land ⟨E, F⟩ Cgr ⟨H, I⟩))$
26	25	3adant3r1	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to (⟨D, ⟨E, F⟩⟩ Cgr3 ⟨G, ⟨H, I⟩⟩ \leftrightarrow (⟨D, E⟩ Cgr ⟨G, H⟩ \land ⟨D, F⟩ Cgr ⟨G, I⟩ \land ⟨E, F⟩ Cgr ⟨H, I⟩))$
27	19 24 26	3imtr4d	$⊢ (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)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land I \in 𝔼 (N)))) \to ((⟨A, ⟨B, C⟩⟩ Cgr3 ⟨D, ⟨E, F⟩⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨G, ⟨H, I⟩⟩) \to ⟨D, ⟨E, F⟩⟩ Cgr3 ⟨G, ⟨H, I⟩⟩)$

Metamath Proof Explorer

Theorem cgr3tr4

Proof