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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmid.1 | |- A e. CH |
|
2 | ssid | |- A C_ A |
|
3 | 1 1 2 | lecmii | |- A C_H A |