Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  latledi Structured version   Unicode version

Theorem latledi 14520
 Description: An ortholattice is distributive in one ordering direction. (ledi 23044 analog.) (Contributed by NM, 7-Nov-2011.)
Hypotheses
Ref Expression
latledi.b
latledi.l
latledi.j
latledi.m
Assertion
Ref Expression
latledi

Proof of Theorem latledi
StepHypRef Expression
1 latledi.b . . . . 5
2 latledi.l . . . . 5
3 latledi.m . . . . 5
41, 2, 3latmle1 14507 . . . 4
61, 2, 3latmle1 14507 . . . 4
81, 3latmcl 14482 . . . . . 6
983adant3r3 1165 . . . . 5
101, 3latmcl 14482 . . . . . 6
11103adant3r2 1164 . . . . 5
12 simpr1 964 . . . . 5
139, 11, 123jca 1135 . . . 4
14 latledi.j . . . . 5
151, 2, 14latjle12 14493 . . . 4
1613, 15syldan 458 . . 3
175, 7, 16mpbi2and 889 . 2
181, 2, 3latmle2 14508 . . . 4
201, 2, 3latmle2 14508 . . . 4
22 simpl 445 . . . 4
23 simpr2 965 . . . 4
24 simpr3 966 . . . 4
251, 2, 14latjlej12 14498 . . . 4
2622, 9, 23, 11, 24, 25syl122anc 1194 . . 3
2719, 21, 26mp2and 662 . 2
281, 14latjcl 14481 . . . 4
2922, 9, 11, 28syl3anc 1185 . . 3
301, 14latjcl 14481 . . . 4