Description: An ortholattice is distributive in one ordering direction. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ledi.1 | ||
ledi.2 | |||
ledi.3 | |||
Assertion | lediri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ledi.1 | ||
2 | ledi.2 | ||
3 | ledi.3 | ||
4 | 3 1 2 | ledii | |
5 | incom | ||
6 | incom | ||
7 | 5 6 | oveq12i | |
8 | incom | ||
9 | 4 7 8 | 3sstr4i |