Description: A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996) (Revised by Mario Carneiro, 10-May-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | soi.1 | ||
soi.2 | |||
Assertion | soirri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | soi.1 | ||
2 | soi.2 | ||
3 | sonr | ||
4 | 1 3 | mpan | |
5 | 4 | adantl | |
6 | 2 | brel | |
7 | 6 | con3i | |
8 | 5 7 | pm2.61i |