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

Theorem cdlemn11a 31844
 Description: Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.)
Hypotheses
Ref Expression
cdlemn11a.b
cdlemn11a.l
cdlemn11a.j
cdlemn11a.a
cdlemn11a.h
cdlemn11a.p
cdlemn11a.o
cdlemn11a.t
cdlemn11a.r
cdlemn11a.e
cdlemn11a.i
cdlemn11a.J
cdlemn11a.u
cdlemn11a.d
cdlemn11a.s
cdlemn11a.f
cdlemn11a.g
Assertion
Ref Expression
cdlemn11a
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()   ()   ()   ()   ()   ()

Proof of Theorem cdlemn11a
StepHypRef Expression
1 simp1 957 . . . . 5
2 cdlemn11a.l . . . . . . 7
3 cdlemn11a.a . . . . . . 7
4 cdlemn11a.h . . . . . . 7
5 cdlemn11a.p . . . . . . 7
62, 3, 4, 5lhpocnel2 30655 . . . . . 6
763ad2ant1 978 . . . . 5
8 simp22 991 . . . . 5
9 cdlemn11a.t . . . . . 6
10 cdlemn11a.g . . . . . 6
112, 3, 4, 9, 10ltrniotacl 31215 . . . . 5
121, 7, 8, 11syl3anc 1184 . . . 4
13 tendospid 31654 . . . 4
1412, 13syl 16 . . 3
1514eqcomd 2440 . 2
16 cdlemn11a.e . . . 4
174, 9, 16tendoidcl 31405 . . 3