Metamath Proof Explorer


Theorem sonr

Description: A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995)

Ref Expression
Assertion sonr
|- ( ( R Or A /\ B e. A ) -> -. B R B )

Proof

Step Hyp Ref Expression
1 sopo
 |-  ( R Or A -> R Po A )
2 poirr
 |-  ( ( R Po A /\ B e. A ) -> -. B R B )
3 1 2 sylan
 |-  ( ( R Or A /\ B e. A ) -> -. B R B )