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

Theorem latnlej2 16269
 Description: An idiom to express that a lattice element differs from two others. (Contributed by NM, 10-Jul-2012.)
Hypotheses
Ref Expression
latlej.b
latlej.l
latlej.j
Assertion
Ref Expression
latnlej2

Proof of Theorem latnlej2
StepHypRef Expression
1 latlej.b . . . . . . 7
2 latlej.l . . . . . . 7
3 latlej.j . . . . . . 7
41, 2, 3latlej1 16258 . . . . . 6
543adant3r1 1214 . . . . 5
6 simpl 458 . . . . . 6
7 simpr1 1011 . . . . . 6
8 simpr2 1012 . . . . . 6
91, 3latjcl 16249 . . . . . . 7
1093adant3r1 1214 . . . . . 6
111, 2lattr 16254 . . . . . 6
126, 7, 8, 10, 11syl13anc 1266 . . . . 5
135, 12mpan2d 678 . . . 4
1413con3d 138 . . 3
151, 2, 3latlej2 16259 . . . . . 6
16153adant3r1 1214 . . . . 5
17 simpr3 1013 . . . . . 6
181, 2lattr 16254 . . . . . 6
196, 7, 17, 10, 18syl13anc 1266 . . . . 5
2016, 19mpan2d 678 . . . 4
2120con3d 138 . . 3