Theorem sonr

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

	Ref	Expression
Assertion	sonr	$$⊢\left(R\mathrm{Or}A\wedge B\in A\right)\to \neg BRB$$

Proof

Step	Hyp	Ref	Expression
1		sopo	$$⊢R\mathrm{Or}A\to R\mathrm{Po}A$$
2		poirr	$$⊢\left(R\mathrm{Po}A\wedge B\in A\right)\to \neg BRB$$
3	1 2	sylan	$$⊢\left(R\mathrm{Or}A\wedge B\in A\right)\to \neg BRB$$