Metamath Proof Explorer


Theorem sonr

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

Ref Expression
Assertion sonr ( ( 𝑅 Or 𝐴𝐵𝐴 ) → ¬ 𝐵 𝑅 𝐵 )

Proof

Step Hyp Ref Expression
1 sopo ( 𝑅 Or 𝐴𝑅 Po 𝐴 )
2 poirr ( ( 𝑅 Po 𝐴𝐵𝐴 ) → ¬ 𝐵 𝑅 𝐵 )
3 1 2 sylan ( ( 𝑅 Or 𝐴𝐵𝐴 ) → ¬ 𝐵 𝑅 𝐵 )