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

Theorem dalemsly 30389
 Description: Lemma for dath 30470. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.)
Hypotheses
Ref Expression
dalema.ph
dalemc.l
dalemc.j
dalemc.a
dalemsly.z
Assertion
Ref Expression
dalemsly

Proof of Theorem dalemsly
StepHypRef Expression
1 dalema.ph . . . . . . 7
21dalemkelat 30358 . . . . . 6
3 dalemc.a . . . . . . 7
41, 3dalemseb 30376 . . . . . 6
5 dalemc.j . . . . . . 7
61, 5, 3dalemtjueb 30381 . . . . . 6
7 eqid 2435 . . . . . . 7
8 dalemc.l . . . . . . 7
97, 8, 5latlej1 14481 . . . . . 6
102, 4, 6, 9syl3anc 1184 . . . . 5
111dalemkehl 30357 . . . . . 6
121dalemsea 30363 . . . . . 6
131dalemtea 30364 . . . . . 6
141dalemuea 30365 . . . . . 6
155, 3hlatjass 30104 . . . . . 6
1611, 12, 13, 14, 15syl13anc 1186 . . . . 5
1710, 16breqtrrd 4230 . . . 4
18 dalemsly.z . . . 4
1917, 18syl6breqr 4244 . . 3