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

Theorem dalem35 30504
 Description: Lemma for dath 30533. Analog of dalem24 30494 for . (Contributed by NM, 3-Aug-2012.)
Hypotheses
Ref Expression
dalem.ph
dalem.l
dalem.j
dalem.a
dalem.ps
dalem34.m
dalem34.o
dalem34.y
dalem34.z
dalem34.i
Assertion
Ref Expression
dalem35

Proof of Theorem dalem35
StepHypRef Expression
1 dalem.ph . . . . 5
2 dalem.l . . . . 5
3 dalem.j . . . . 5
4 dalem.a . . . . 5
5 dalem34.y . . . . 5
6 dalem34.z . . . . 5
71, 2, 3, 4, 5, 6dalemrot 30454 . . . 4
91, 2, 3, 4, 5, 6dalemrotyz 30455 . . . 4
11 dalem.ps . . . . 5
121, 2, 3, 4, 11, 5dalemrotps 30488 . . . 4
14 biid 228 . . . 4
15 biid 228 . . . 4
16 dalem34.m . . . 4
17 dalem34.o . . . 4
18 eqid 2436 . . . 4
19 eqid 2436 . . . 4
20 dalem34.i . . . 4
2114, 2, 3, 4, 15, 16, 17, 18, 19, 20dalem30 30499 . . 3
228, 10, 13, 21syl3anc 1184 . 2
231, 3, 4dalemqrprot 30445 . . . . 5
2423, 5syl6reqr 2487 . . . 4
2524breq2d 4224 . . 3