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

Theorem cdleme21 29215
 Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd line on p. 115. , , , , , represent s2, f(s), fs(r), t2, f(t), ft(r) respectively. Combine cdleme18d 29173 and cdleme21j 29214 to eliminate existence condition, proving fs(r) = ft(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.)
Hypotheses
Ref Expression
cdleme21.l
cdleme21.j
cdleme21.m
cdleme21.a
cdleme21.h
cdleme21.u
cdleme21.f
cdleme21g.g
cdleme21g.d
cdleme21g.y
cdleme21g.n
cdleme21g.o
Assertion
Ref Expression
cdleme21

Proof of Theorem cdleme21
StepHypRef Expression
1 simpl1 963 . . 3
2 simpl2 964 . . 3
3 simpl3l 1015 . . 3
4 simpl3r 1016 . . 3
5 simpr 449 . . 3
6 cdleme21.l . . . 4
7 cdleme21.j . . . 4
8 cdleme21.m . . . 4
9 cdleme21.a . . . 4
10 cdleme21.h . . . 4
11 cdleme21.u . . . 4
12 cdleme21.f . . . 4
13 cdleme21g.g . . . 4
14 cdleme21g.d . . . 4
15 cdleme21g.y . . . 4
16 cdleme21g.n . . . 4
17 cdleme21g.o . . . 4
186, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17cdleme21j 29214 . . 3
191, 2, 3, 4, 5, 18syl113anc 1199 . 2
20 simpl1 963 . . 3
21 simpl2 964 . . 3
22 simp3ll 1031 . . . 4
24 simp3r3 1070 . . . . 5
25 simp3r1 1068 . . . . 5
26 simp3r2 1069 . . . . 5
2724, 25, 263jca 1137 . . . 4