Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Geometry in the Euclidean space
Congruence properties
cgrcomand
Next ⟩
cgrtr
Metamath Proof Explorer
Ascii
Unicode
Theorem
cgrcomand
Description:
Deduction form of
cgrcom
.
(Contributed by
Scott Fenton
, 13-Oct-2013)
Ref
Expression
Hypotheses
cgrcomand.1
⊢
φ
→
N
∈
ℕ
cgrcomand.2
⊢
φ
→
A
∈
𝔼
⁡
N
cgrcomand.3
⊢
φ
→
B
∈
𝔼
⁡
N
cgrcomand.4
⊢
φ
→
C
∈
𝔼
⁡
N
cgrcomand.5
⊢
φ
→
D
∈
𝔼
⁡
N
cgrcomand.6
⊢
φ
∧
ψ
→
A
B
Cgr
C
D
Assertion
cgrcomand
⊢
φ
∧
ψ
→
C
D
Cgr
A
B
Proof
Step
Hyp
Ref
Expression
1
cgrcomand.1
⊢
φ
→
N
∈
ℕ
2
cgrcomand.2
⊢
φ
→
A
∈
𝔼
⁡
N
3
cgrcomand.3
⊢
φ
→
B
∈
𝔼
⁡
N
4
cgrcomand.4
⊢
φ
→
C
∈
𝔼
⁡
N
5
cgrcomand.5
⊢
φ
→
D
∈
𝔼
⁡
N
6
cgrcomand.6
⊢
φ
∧
ψ
→
A
B
Cgr
C
D
7
cgrcom
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
→
A
B
Cgr
C
D
↔
C
D
Cgr
A
B
8
1
2
3
4
5
7
syl122anc
⊢
φ
→
A
B
Cgr
C
D
↔
C
D
Cgr
A
B
9
8
adantr
⊢
φ
∧
ψ
→
A
B
Cgr
C
D
↔
C
D
Cgr
A
B
10
6
9
mpbid
⊢
φ
∧
ψ
→
C
D
Cgr
A
B