This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in C_{ℋ}$
	Assertion	cmidi	$⊢ A 𝐶_{ℋ} A$

Step	Hyp	Ref	Expression
1		cmid.1	$⊢ A \in C_{ℋ}$
2		ssid	$⊢ A \subseteq A$
3	1 1 2	lecmii	$⊢ A 𝐶_{ℋ} A$