Metamath Proof Explorer


Theorem so3nr

Description: A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996)

Ref Expression
Assertion so3nr ROrABACADA¬BRCCRDDRB

Proof

Step Hyp Ref Expression
1 sopo ROrARPoA
2 po3nr RPoABACADA¬BRCCRDDRB
3 1 2 sylan ROrABACADA¬BRCCRDDRB