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 )