Metamath Proof Explorer

Theorem cgrrflx

Description: Reflexivity law for congruence. Theorem 2.1 of Schwabhauser p. 27. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion cgrrflx ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→ABCgrAB

Proof

Step Hyp Ref Expression
1 simp1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→N∈ℕ
2 simp3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→B∈𝔼⁡N
3 simp2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→A∈𝔼⁡N
4 axcgrrflx ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N→BACgrAB
5 4 3com23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→BACgrAB
6 1 2 3 3 2 3 2 5 5 cgrtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→ABCgrAB