Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dihmeetlem12N Structured version   Unicode version

Theorem dihmeetlem12N 32117
 Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dihmeetlem9.b
dihmeetlem9.l
dihmeetlem9.h
dihmeetlem9.j
dihmeetlem9.m
dihmeetlem9.a
dihmeetlem9.u
dihmeetlem9.s
dihmeetlem9.i
Assertion
Ref Expression
dihmeetlem12N

Proof of Theorem dihmeetlem12N
StepHypRef Expression
1 simpl1 961 . . . 4
2 simpl2 962 . . . 4
3 simpl3 963 . . . 4
4 simpr1 964 . . . 4
5 simpr2 965 . . . 4
6 simpr3 966 . . . 4
7 dihmeetlem9.b . . . . 5
8 dihmeetlem9.l . . . . 5
9 dihmeetlem9.h . . . . 5
10 dihmeetlem9.j . . . . 5
11 dihmeetlem9.m . . . . 5
12 dihmeetlem9.a . . . . 5
13 dihmeetlem9.u . . . . 5
14 dihmeetlem9.s . . . . 5
15 dihmeetlem9.i . . . . 5
167, 8, 9, 10, 11, 12, 13, 14, 15dihmeetlem8N 32113 . . . 4
171, 2, 3, 4, 5, 6, 16syl312anc 1206 . . 3
1817ineq1d 3542 . 2
197, 8, 9, 10, 11, 12, 13, 14, 15dihmeetlem11N 32116 . . 3