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

Theorem latledi 14473
 Description: An ortholattice is distributive in one ordering direction. (ledi 22995 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 14460 . . . 4
61, 2, 3latmle1 14460 . . . 4
81, 3latmcl 14435 . . . . . 6
983adant3r3 1164 . . . . 5
101, 3latmcl 14435 . . . . . 6
11103adant3r2 1163 . . . . 5
12 simpr1 963 . . . . 5
139, 11, 123jca 1134 . . . 4
14 latledi.j . . . . 5
151, 2, 14latjle12 14446 . . . 4
1613, 15syldan 457 . . 3
175, 7, 16mpbi2and 888 . 2
181, 2, 3latmle2 14461 . . . 4
201, 2, 3latmle2 14461 . . . 4
22 simpl 444 . . . 4
23 simpr2 964 . . . 4
24 simpr3 965 . . . 4
251, 2, 14latjlej12 14451 . . . 4
2622, 9, 23, 11, 24, 25syl122anc 1193 . . 3
2719, 21, 26mp2and 661 . 2
281, 14latjcl 14434 . . . 4
2922, 9, 11, 28syl3anc 1184 . . 3
301, 14latjcl 14434 . . . 4