Metamath Proof Explorer
Description: A lattice ordering is transitive. Deduction version of lattr .
(Contributed by NM, 3-Sep-2012)
|
|
Ref |
Expression |
|
Hypotheses |
lattrd.b |
|
|
|
lattrd.l |
|
|
|
lattrd.1 |
|
|
|
lattrd.2 |
|
|
|
lattrd.3 |
|
|
|
lattrd.4 |
|
|
|
lattrd.5 |
|
|
|
lattrd.6 |
|
|
Assertion |
lattrd |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
lattrd.b |
|
2 |
|
lattrd.l |
|
3 |
|
lattrd.1 |
|
4 |
|
lattrd.2 |
|
5 |
|
lattrd.3 |
|
6 |
|
lattrd.4 |
|
7 |
|
lattrd.5 |
|
8 |
|
lattrd.6 |
|
9 |
1 2
|
lattr |
|
10 |
3 4 5 6 9
|
syl13anc |
|
11 |
7 8 10
|
mp2and |
|