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 e. CH
Assertion cmidi
|- A C_H A

Proof

Step Hyp Ref Expression
1 cmid.1
 |-  A e. CH
2 ssid
 |-  A C_ A
3 1 1 2 lecmii
 |-  A C_H A