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

Theorem 3dimlem4OLDN 29654
 Description: Lemma for 3dim1 29656. (Contributed by NM, 25-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
3dim0.j
3dim0.l
3dim0.a
Assertion
Ref Expression
3dimlem4OLDN

Proof of Theorem 3dimlem4OLDN
StepHypRef Expression
1 simp2l 981 . 2
2 simp2r 982 . . 3
3 simp11 985 . . . . . 6
4 simp2l 981 . . . . . 6
5 simp12 986 . . . . . 6
6 simp13 987 . . . . . 6
7 simp3l 983 . . . . . . 7
87necomd 2529 . . . . . 6
9 3dim0.l . . . . . . 7
10 3dim0.j . . . . . . 7
11 3dim0.a . . . . . . 7
129, 10, 11hlatexch2 29585 . . . . . 6
133, 4, 5, 6, 8, 12syl131anc 1195 . . . . 5
1410, 11hlatjcom 29557 . . . . . . 7
153, 6, 4, 14syl3anc 1182 . . . . . 6
1615breq2d 4035 . . . . 5
1713, 16sylibrd 225 . . . 4
192, 18mtod 168 . 2
20 simp3 957 . . 3
21 hllat 29553 . . . . . . . 8
223, 21syl 15 . . . . . . 7
23 eqid 2283 . . . . . . . . 9
2423, 11atbase 29479 . . . . . . . 8
256, 24syl 15 . . . . . . 7
2623, 11atbase 29479 . . . . . . . 8
274, 26syl 15 . . . . . . 7
2823, 11atbase 29479 . . . . . . . 8
295, 28syl 15 . . . . . . 7
3023, 10latjrot 14206 . . . . . . 7
3122, 25, 27, 29, 30syl13anc 1184 . . . . . 6
3231breq2d 4035 . . . . 5
33 simp2r 982 . . . . . 6
3423, 10, 11hlatjcl 29556 . . . . . . 7
353, 6, 4, 34syl3anc 1182 . . . . . 6
36 simp3r 984 . . . . . 6
3723, 9, 10, 11hlexch1 29571 . . . . . 6
383, 33, 5, 35, 36, 37syl131anc 1195 . . . . 5
3932, 38sylbird 226 . . . 4