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 𝐴C
Assertion cmidi 𝐴 𝐶 𝐴

Proof

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