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

Theorem dalem4 34862
 Description: Lemma for dalemdnee 34863. (Contributed by NM, 10-Aug-2012.)
Hypotheses
Ref Expression
dalema.ph
dalemc.l
dalemc.j
dalemc.a
dalem3.m
dalem3.o
dalem3.y
dalem3.z
dalem3.d
dalem3.e
Assertion
Ref Expression
dalem4

Proof of Theorem dalem4
StepHypRef Expression
1 dalema.ph . . . . 5
2 dalemc.l . . . . 5
3 dalemc.j . . . . 5
4 dalemc.a . . . . 5
51, 2, 3, 4dalemswapyz 34853 . . . 4
7 dalem3.d . . . . . 6
81dalemkelat 34821 . . . . . . 7
91, 3, 4dalempjqeb 34842 . . . . . . 7
101, 3, 4dalemsjteb 34843 . . . . . . 7
11 eqid 2467 . . . . . . . 8
12 dalem3.m . . . . . . . 8
1311, 12latmcom 15579 . . . . . . 7
148, 9, 10, 13syl3anc 1228 . . . . . 6
157, 14syl5eq 2520 . . . . 5
1615neeq1d 2744 . . . 4
1716biimpa 484 . . 3
18 biid 236 . . . 4
19 dalem3.o . . . 4
20 dalem3.z . . . 4
21 dalem3.y . . . 4
22 eqid 2467 . . . 4
23 eqid 2467 . . . 4
2418, 2, 3, 4, 12, 19, 20, 21, 22, 23dalem3 34861 . . 3
256, 17, 24syl2anc 661 . 2
27 dalem3.e . . . 4
281dalemkehl 34820 . . . . . 6
291dalemqea 34824 . . . . . 6
301dalemrea 34825 . . . . . 6
3111, 3, 4hlatjcl 34564 . . . . . 6
3228, 29, 30, 31syl3anc 1228 . . . . 5
331, 3, 4dalemtjueb 34844 . . . . 5
3411, 12latmcom 15579 . . . . 5
358, 32, 33, 34syl3anc 1228 . . . 4
3627, 35syl5eq 2520 . . 3