Metamath Proof Explorer


Theorem cmidi

Description: The commutes relation is reflexive. (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypothesis cmid.1 A C
Assertion cmidi A 𝐶 A

Proof

Step Hyp Ref Expression
1 cmid.1 A C
2 ssid A A
3 1 1 2 lecmii A 𝐶 A