Metamath Proof Explorer


Theorem lediri

Description: An ortholattice is distributive in one ordering direction. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses ledi.1 A C
ledi.2 B C
ledi.3 C C
Assertion lediri A C B C A B C

Proof

Step Hyp Ref Expression
1 ledi.1 A C
2 ledi.2 B C
3 ledi.3 C C
4 3 1 2 ledii C A C B C A B
5 incom A C = C A
6 incom B C = C B
7 5 6 oveq12i A C B C = C A C B
8 incom A B C = C A B
9 4 7 8 3sstr4i A C B C A B C