cdlemg27b - Mathbox for Norm Megill

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

Theorem cdlemg27b 34257

Description: TODO: Fix comment. (Contributed by NM, 28-May-2013.)

**Hypotheses**
Ref	Expression
cdlemg12.l
cdlemg12.j	$.\/$
cdlemg12.m	$./\$
cdlemg12.a
cdlemg12.h
cdlemg12.t
cdlemg12b.r
cdlemg31.n	$.\/$ $./\$ $.\/$

**Assertion**
Ref	Expression
cdlemg27b	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$

**Proof of Theorem cdlemg27b**
Step	Hyp	Ref	Expression
1		simp11 1037	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
2		simp12 1038	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
3		simp13 1039	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
4		simp22 1041	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
5		simp23l 1128	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
6		simp31 1043	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
7		cdlemg12.l	. . . . . 6
8		cdlemg12.j	. . . . . 6 $.\/$
9		cdlemg12.m	. . . . . 6 $./\$
10		cdlemg12.a	. . . . . 6
11		cdlemg12.h	. . . . . 6
12		cdlemg12.t	. . . . . 6
13		cdlemg12b.r	. . . . . 6
14		cdlemg31.n	. . . . . 6 $.\/$ $./\$ $.\/$
15	7, 8, 9, 10, 11, 12, 13, 14	cdlemg31b0a 34256	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
16	1, 2, 3, 4, 5, 6, 15	syl132anc 1285	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $\/$
17		simp23r 1129	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
18	17	adantr 467	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $\/$
19		simp11l 1118	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
20	19	adantr 467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
21		hlatl 32920	. . . . . . . . 9
22	20, 21	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
23		simpl21 1085	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
24		simpr 463	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
25	7, 10	atcmp 32871	. . . . . . . 8 $/\$ $/\$
26	22, 23, 24, 25	syl3anc 1267	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
27	26	necon3bbid 2660	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
28	19	adantr 467	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
29	28, 21	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
30		simpl21 1085	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
31		eqid 2450	. . . . . . . . . 10
32	7, 31, 10	atnle0 32869	. . . . . . . . 9 $/\$
33	29, 30, 32	syl2anc 666	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
34		simpr 463	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
35	34	breq2d 4413	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
36	33, 35	mtbird 303	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
37	17	adantr 467	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
38	36, 37	2thd 244	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
39	27, 38	jaodan 793	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $\/$
40	18, 39	mpbird 236	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $\/$
41	16, 40	mpdan 673	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
42		simp32 1044	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
43		hllat 32923	. . . . . . . 8
44	19, 43	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
45		simp21 1040	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
46		eqid 2450	. . . . . . . . 9
47	46, 10	atbase 32849	. . . . . . . 8
48	45, 47	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
49		simp12l 1120	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
50		simp22l 1126	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
51	46, 8, 10	hlatjcl 32926	. . . . . . . 8 $/\$ $/\$ $.\/$
52	19, 49, 50, 51	syl3anc 1267	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
53		simp13l 1122	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
54		simp33 1045	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
55	7, 10, 11, 12, 13	trlat 33729	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
56	1, 2, 5, 54, 55	syl112anc 1271	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
57	46, 8, 10	hlatjcl 32926	. . . . . . . 8 $/\$ $/\$ $.\/$
58	19, 53, 56, 57	syl3anc 1267	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
59	46, 7, 9	latlem12 16317	. . . . . . 7 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
60	44, 48, 52, 58, 59	syl13anc 1269	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
61	14	breq2i 4409	. . . . . 6 $.\/$ $./\$ $.\/$
62	60, 61	syl6bbr 267	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
63	62	biimpd 211	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
64	42, 63	mpand 680	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
65	41, 64	mtod 181	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
66	7, 11, 12, 13	trlle 33744	. . . . 5 $/\$ $/\$
67	1, 5, 66	syl2anc 666	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
68		simp13r 1123	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
69		nbrne2 4420	. . . 4 $/\$
70	67, 68, 69	syl2anc 666	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
71	7, 8, 10	hlatexch1 32954	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
72	19, 56, 45, 53, 70, 71	syl131anc 1280	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
73	65, 72	mtod 181	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886

wne 2621 class class class wbr 4401

cfv 5581 (class class class)co 6288

cbs 15114

cple 15190

cjn 16182

cmee 16183

cp0 16276

clat 16284

catm 32823

cal 32824

chlt 32910

clh 33543

cltrn 33660

ctrl 33718

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-ral 2741 df-rex 2742 df-reu 2743 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-op 3974 df-uni 4198 df-iun 4279 df-iin 4280 df-br 4402 df-opab 4461 df-mpt 4462 df-id 4748 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-1st 6790 df-2nd 6791 df-map 7471 df-preset 16166 df-poset 16184 df-plt 16197 df-lub 16213 df-glb 16214 df-join 16215 df-meet 16216 df-p0 16278 df-p1 16279 df-lat 16285 df-clat 16347 df-oposet 32736 df-ol 32738 df-oml 32739 df-covers 32826 df-ats 32827 df-atl 32858 df-cvlat 32882 df-hlat 32911 df-llines 33057 df-psubsp 33062 df-pmap 33063 df-padd 33355 df-lhyp 33547 df-laut 33548 df-ldil 33663 df-ltrn 33664 df-trl 33719

This theorem is referenced by: cdlemg28b 34264

W3C validator