po3nr

Description: A partial order has no 3-cycle loops. (Contributed by NM, 27-Mar-1997)

		Ref	Expression
	Assertion	po3nr	$⊢ (R Po A \land (B \in A \land C \in A \land D \in A)) \to \neg (B R C \land C R D \land D R B)$

Step	Hyp	Ref	Expression
1		po2nr	$⊢ (R Po A \land (B \in A \land D \in A)) \to \neg (B R D \land D R B)$
2	1	3adantr2	$⊢ (R Po A \land (B \in A \land C \in A \land D \in A)) \to \neg (B R D \land D R B)$
3		df-3an	$⊢ (B R C \land C R D \land D R B) \leftrightarrow ((B R C \land C R D) \land D R B)$
4		potr	$⊢ (R Po A \land (B \in A \land C \in A \land D \in A)) \to ((B R C \land C R D) \to B R D)$
5	4	anim1d	$⊢ (R Po A \land (B \in A \land C \in A \land D \in A)) \to (((B R C \land C R D) \land D R B) \to (B R D \land D R B))$
6	3 5	syl5bi	$⊢ (R Po A \land (B \in A \land C \in A \land D \in A)) \to ((B R C \land C R D \land D R B) \to (B R D \land D R B))$
7	2 6	mtod	$⊢ (R Po A \land (B \in A \land C \in A \land D \in A)) \to \neg (B R C \land C R D \land D R B)$

Metamath Proof Explorer