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

Theorem cdleme50eq 30730
 Description: Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
Hypotheses
Ref Expression
cdlemef50.b
cdlemef50.l
cdlemef50.j
cdlemef50.m
cdlemef50.a
cdlemef50.h
cdlemef50.u
cdlemef50.d
cdlemefs50.e
cdlemef50.f
Assertion
Ref Expression
cdleme50eq
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,   ,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,
Allowed substitution hints:   ()   (,)   (,,,,)

Proof of Theorem cdleme50eq
StepHypRef Expression
1 cdlemef50.b . . . 4
2 cdlemef50.l . . . 4
3 cdlemef50.j . . . 4
4 cdlemef50.m . . . 4
5 cdlemef50.a . . . 4
6 cdlemef50.h . . . 4
7 cdlemef50.u . . . 4
8 cdlemef50.d . . . 4
9 cdlemefs50.e . . . 4
10 cdlemef50.f . . . 4
111, 2, 3, 4, 5, 6, 7, 8, 9, 10cdleme50lebi 30729 . . 3
121, 2, 3, 4, 5, 6, 7, 8, 9, 10cdleme50lebi 30729 . . . 4
1312ancom2s 777 . . 3
1411, 13anbi12d 691 . 2
15 simpl1l 1006 . . . 4
16 hllat 29553 . . . 4
1715, 16syl 15 . . 3
18 simprl 732 . . 3
19 simprr 733 . . 3
201, 2latasymb 14160 . . 3
2117, 18, 19, 20syl3anc 1182 . 2
22 eqid 2283 . . . . 5
23 eqid 2283 . . . . 5
24 biid 227 . . . . . 6
25 vex 2791 . . . . . . 7
268, 22cdleme31sc 30573 . . . . . . 7
2725, 26ax-mp 8 . . . . . 6
2824, 27ifbieq2i 3584 . . . . 5
29 eqid 2283 . . . . 5
301, 2, 3, 4, 5, 6, 7, 22, 8, 9, 23, 28, 29, 10cdleme32fvcl 30629 . . . 4