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

Theorem cdleme21 31134
 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 31092 and cdleme21j 31133 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
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpl1 960 . . 3
2 simpl2 961 . . 3
3 simpl3l 1012 . . 3
4 simpl3r 1013 . . 3
5 simpr 448 . . 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 31133 . . 3
191, 2, 3, 4, 5, 18syl113anc 1196 . 2
20 simpl1 960 . . 3
21 simpl2 961 . . 3
22 simp3ll 1028 . . . 4
24 simp3r3 1067 . . . . 5
25 simp3r1 1065 . . . . 5
26 simp3r2 1066 . . . . 5
2724, 25, 263jca 1134 . . . 4