Metamath Proof Explorer

Theorem cgrid2

Description: Identity law for congruence. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion cgrid2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AACgrBC→B=C

Proof

Step Hyp Ref Expression
1 simpl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→N∈ℕ
2 simpr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→A∈𝔼⁡N
3 simpr2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B∈𝔼⁡N
4 simpr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→C∈𝔼⁡N
5 cgrcom ⊢N∈ℕ∧A∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AACgrBC↔BCCgrAA
6 1 2 2 3 4 5 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AACgrBC↔BCCgrAA
7 3anrot ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N↔B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N
8 axcgrid ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→BCCgrAA→B=C
9 7 8 sylan2b ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BCCgrAA→B=C
10 6 9 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AACgrBC→B=C