Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Geometry in the Euclidean space
Properties relating betweenness and congruence
cgr3permute4
Next ⟩
cgr3permute5
Metamath Proof Explorer
Ascii
Unicode
Theorem
cgr3permute4
Description:
Permutation law for three-place congruence.
(Contributed by
Scott Fenton
, 5-Oct-2013)
Ref
Expression
Assertion
cgr3permute4
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
A
B
C
Cgr3
D
E
F
↔
C
A
B
Cgr3
F
D
E
Proof
Step
Hyp
Ref
Expression
1
cgr3permute3
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
A
B
C
Cgr3
D
E
F
↔
B
C
A
Cgr3
E
F
D
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
cgr3permute3
⊢
N
∈
ℕ
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
A
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
→
B
C
A
Cgr3
E
F
D
↔
C
A
B
Cgr3
F
D
E
6
2
3
4
5
syl3anb
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
B
C
A
Cgr3
E
F
D
↔
C
A
B
Cgr3
F
D
E
7
1
6
bitrd
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
A
B
C
Cgr3
D
E
F
↔
C
A
B
Cgr3
F
D
E