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

Theorem cdlemk53b 31680
 Description: Lemma for cdlemk53 31681. (Contributed by NM, 26-Jul-2013.)
Hypotheses
Ref Expression
cdlemk5.b
cdlemk5.l
cdlemk5.j
cdlemk5.m
cdlemk5.a
cdlemk5.h
cdlemk5.t
cdlemk5.r
cdlemk5.z
cdlemk5.y
cdlemk5.x
Assertion
Ref Expression
cdlemk53b
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,,,   ,,   ,   ,,   ,,   ,,,   ,,   ,,,   ,   ,,,   ,,,   ,,,   ,,   ,,   ,,   ,,,   ,   ,   ,,,
Allowed substitution hints:   (,,)   (,)   (,)

Proof of Theorem cdlemk53b
StepHypRef Expression
1 simp1l 981 . . . . . 6
2 simp211 1095 . . . . . . . 8
3 simp212 1096 . . . . . . . 8
42, 3jca 519 . . . . . . 7
5 simp31 993 . . . . . . 7
6 simp213 1097 . . . . . . 7
7 simp23 992 . . . . . . 7
8 simp1r 982 . . . . . . 7
9 cdlemk5.b . . . . . . . 8
10 cdlemk5.l . . . . . . . 8
11 cdlemk5.j . . . . . . . 8
12 cdlemk5.m . . . . . . . 8
13 cdlemk5.a . . . . . . . 8
14 cdlemk5.h . . . . . . . 8
15 cdlemk5.t . . . . . . . 8
16 cdlemk5.r . . . . . . . 8
17 cdlemk5.z . . . . . . . 8
18 cdlemk5.y . . . . . . . 8
19 cdlemk5.x . . . . . . . 8
209, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19cdlemk35s-id 31662 . . . . . . 7
211, 4, 5, 6, 7, 8, 20syl132anc 1202 . . . . . 6
229, 14, 15ltrn1o 30848 . . . . . 6
231, 21, 22syl2anc 643 . . . . 5
2423adantr 452 . . . 4
25 f1of 5666 . . . 4
26 fcoi2 5610 . . . 4
2724, 25, 263syl 19 . . 3
28 simpl1l 1008 . . . . 5
292, 6, 83jca 1134 . . . . . 6
3029adantr 452 . . . . 5
31 simpl23 1037 . . . . 5
32 simpr 448 . . . . 5
339, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19cdlemkid 31660 . . . . 5
3428, 30, 31, 32, 33syl112anc 1188 . . . 4
3534coeq1d 5026 . . 3
3632coeq1d 5026 . . . . 5
37 simpl31 1038 . . . . . . 7
389, 14, 15ltrn1o 30848 . . . . . . 7
3928, 37, 38syl2anc 643 . . . . . 6
40 f1of 5666 . . . . . 6
41 fcoi2 5610 . . . . . 6
4239, 40, 413syl 19 . . . . 5
4336, 42eqtrd 2467 . . . 4
4443csbeq1d 3249 . . 3
4527, 35, 443eqtr4rd 2478 . 2
46 simpl1l 1008 . . 3