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

Metamath Proof Explorer

Theorem cmtcomN

Description: Commutation is symmetric. Theorem 2(v) in Kalmbach p. 22. ( cmcmi analog.) (Contributed by NM, 7-Nov-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cmtcom.b	$⊢ B = {Base}_{K}$
	cmtcom.c	$⊢ C = cm (K)$
Assertion	cmtcomN	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow Y C X)$

Proof

Step	Hyp	Ref	Expression
1		cmtcom.b	$⊢ B = {Base}_{K}$
2		cmtcom.c	$⊢ C = cm (K)$
3	1 2	cmtcomlemN	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \to Y C X)$
4	1 2	cmtcomlemN	$⊢ (K \in OML \land Y \in B \land X \in B) \to (Y C X \to X C Y)$
5	4	3com23	$⊢ (K \in OML \land X \in B \land Y \in B) \to (Y C X \to X C Y)$
6	3 5	impbid	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow Y C X)$