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

Theorem mapdh8g 32269
 Description: Part of Part (8) in [Baer] p. 48. Eliminate . TODO: break out in mapdh8e 32267 so we can share hypotheses. Also, look at hypothesis sharing for earlier mapdh8* and mapdh75* stuff. (Contributed by NM, 10-May-2015.)
Hypotheses
Ref Expression
mapdh8a.h
mapdh8a.u
mapdh8a.v
mapdh8a.s
mapdh8a.o
mapdh8a.n
mapdh8a.c LCDual
mapdh8a.d
mapdh8a.r
mapdh8a.q
mapdh8a.j
mapdh8a.m mapd
mapdh8a.i
mapdh8a.k
mapdh8e.f
mapdh8e.mn
mapdh8e.eg
mapdh8e.x
mapdh8e.y
mapdh8e.t
mapdh8e.xy
mapdh8e.xt
mapdh8e.yt
Assertion
Ref Expression
mapdh8g
Distinct variable groups:   ,,   ,,   ,   ,,   ,,   ,   ,,   ,,   ,,   ,,   ,   ,,   ,   ,,   ,   ,,   ,,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   (,)   (,)   ()   (,)

Proof of Theorem mapdh8g
StepHypRef Expression
1 mapdh8a.h . . 3
2 mapdh8a.u . . 3
3 mapdh8a.v . . 3
4 mapdh8a.s . . 3
5 mapdh8a.o . . 3
6 mapdh8a.n . . 3
7 mapdh8a.c . . 3 LCDual
8 mapdh8a.d . . 3
9 mapdh8a.r . . 3
10 mapdh8a.q . . 3
11 mapdh8a.j . . 3
12 mapdh8a.m . . 3 mapd
13 mapdh8a.i . . 3
14 mapdh8a.k . . . 4
16 mapdh8e.f . . . 4
18 mapdh8e.mn . . . 4
20 mapdh8e.eg . . . 4
22 mapdh8e.x . . . 4
24 mapdh8e.y . . . 4
26 mapdh8e.t . . . 4
28 mapdh8e.xy . . . 4
30 mapdh8e.xt . . . 4
32 mapdh8e.yt . . . 4
34 simpr 448 . . 3
351, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31, 33, 34mapdh8e 32267 . 2