Metamath Proof Explorer


Theorem ledii

Description: An ortholattice is distributive in one ordering direction. (Contributed by NM, 6-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses ledi.1 A C
ledi.2 B C
ledi.3 C C
Assertion ledii A B A 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 inss1 A B A
5 inss1 A C A
6 1 2 chincli A B C
7 1 3 chincli A C C
8 6 7 1 chlubii A B A A C A A B A C A
9 4 5 8 mp2an A B A C A
10 inss2 A B B
11 inss2 A C C
12 6 2 7 3 chlej12i A B B A C C A B A C B C
13 10 11 12 mp2an A B A C B C
14 9 13 ssini A B A C A B C