Metamath Proof Explorer


Theorem lejdii

Description: An ortholattice is distributive in one ordering direction (join version). (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 lejdii A B C A B A C

Proof

Step Hyp Ref Expression
1 ledi.1 A C
2 ledi.2 B C
3 ledi.3 C C
4 1 2 chub1i A A B
5 1 3 chub1i A A C
6 4 5 ssini A A B A C
7 inss1 B C B
8 2 1 chub2i B A B
9 7 8 sstri B C A B
10 inss2 B C C
11 3 1 chub2i C A C
12 10 11 sstri B C A C
13 9 12 ssini B C A B A C
14 2 3 chincli B C C
15 1 2 chjcli A B C
16 1 3 chjcli A C C
17 15 16 chincli A B A C C
18 1 14 17 chlubi A A B A C B C A B A C A B C A B A C
19 18 bicomi A B C A B A C A A B A C B C A B A C
20 6 13 19 mpbir2an A B C A B A C