Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Geometry in the Euclidean space
Congruence properties
cgrtr3
Next ⟩
cgrtr3and
Metamath Proof Explorer
Ascii
Unicode
Theorem
cgrtr3
Description:
Transitivity law for congruence.
(Contributed by
Scott Fenton
, 7-Oct-2013)
Ref
Expression
Assertion
cgrtr3
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
A
B
Cgr
E
F
∧
C
D
Cgr
E
F
→
A
B
Cgr
C
D
Proof
Step
Hyp
Ref
Expression
1
simp1
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
N
∈
ℕ
2
simp21
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
A
∈
𝔼
⁡
N
3
simp22
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
B
∈
𝔼
⁡
N
4
simp32
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
E
∈
𝔼
⁡
N
5
simp33
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
F
∈
𝔼
⁡
N
6
simp23
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
C
∈
𝔼
⁡
N
7
simp31
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
D
∈
𝔼
⁡
N
8
simprl
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
∧
A
B
Cgr
E
F
∧
C
D
Cgr
E
F
→
A
B
Cgr
E
F
9
simprr
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
∧
A
B
Cgr
E
F
∧
C
D
Cgr
E
F
→
C
D
Cgr
E
F
10
1
6
7
4
5
9
cgrcomand
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
∧
A
B
Cgr
E
F
∧
C
D
Cgr
E
F
→
E
F
Cgr
C
D
11
1
2
3
4
5
6
7
8
10
cgrtrand
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
∧
A
B
Cgr
E
F
∧
C
D
Cgr
E
F
→
A
B
Cgr
C
D
12
11
ex
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
∧
E
∈
𝔼
⁡
N
∧
F
∈
𝔼
⁡
N
→
A
B
Cgr
E
F
∧
C
D
Cgr
E
F
→
A
B
Cgr
C
D