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

Theorem dalem30 30561
 Description: Lemma for dath 30595. Analog of dalem24 30556 for . (Contributed by NM, 3-Aug-2012.)
Hypotheses
Ref Expression
dalem.ph
dalem.l
dalem.j
dalem.a
dalem.ps
dalem29.m
dalem29.o
dalem29.y
dalem29.z
dalem29.h
Assertion
Ref Expression
dalem30

Proof of Theorem dalem30
StepHypRef Expression
1 dalem.ph . . . . 5
2 dalem.l . . . . 5
3 dalem.j . . . . 5
4 dalem.a . . . . 5
5 dalem29.y . . . . 5
6 dalem29.z . . . . 5
71, 2, 3, 4, 5, 6dalemrot 30516 . . . 4
91, 2, 3, 4, 5, 6dalemrotyz 30517 . . . 4
11 dalem.ps . . . . 5
121, 2, 3, 4, 11, 5dalemrotps 30550 . . . 4
14 biid 229 . . . 4
15 biid 229 . . . 4
16 dalem29.m . . . 4
17 dalem29.o . . . 4
18 eqid 2438 . . . 4
19 eqid 2438 . . . 4
20 dalem29.h . . . 4
2114, 2, 3, 4, 15, 16, 17, 18, 19, 20dalem24 30556 . . 3
228, 10, 13, 21syl3anc 1185 . 2
231, 3, 4dalemqrprot 30507 . . . . 5
2423, 5syl6reqr 2489 . . . 4
2524breq2d 4226 . . 3