cdleme22b - Mathbox for Norm Megill

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

Theorem cdleme22b 36464

Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t $\/$ v =/= p $\/$ q and s

p $\/$ q implies

p $\/$ q. (Contributed by NM, 2-Dec-2012.)

**Hypotheses**
Ref	Expression
cdleme22.l
cdleme22.j	$.\/$
cdleme22.m	$./\$
cdleme22.a
cdleme22.h

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

**Proof of Theorem cdleme22b**
Step	Hyp	Ref	Expression
1		simp1l 1018	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		simp1r1 1090	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
3		simp1r2 1091	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
4		simp1r3 1092	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
5		cdleme22.j	. . . . . . 7 $.\/$
6		cdleme22.a	. . . . . . 7
7		eqid 2454	. . . . . . 7
8	5, 6, 7	llni2 35633	. . . . . 6 $/\$ $/\$ $/\$ $.\/$
9	1, 2, 3, 4, 8	syl31anc 1229	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
10	6, 7	llnneat 35635	. . . . 5 $/\$ $.\/$ $.\/$
11	1, 9, 10	syl2anc 659	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
12		eqid 2454	. . . . . 6
13	12, 7	llnn0 35637	. . . . 5 $/\$ $.\/$ $.\/$
14	1, 9, 13	syl2anc 659	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
15	11, 14	jca 530	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
16		df-ne 2651	. . . . 5 $.\/$ $.\/$
17	16	anbi2i 692	. . . 4 $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
18		pm4.56 493	. . . 4 $.\/$ $/\$ $.\/$ $.\/$ $\/$ $.\/$
19	17, 18	bitri 249	. . 3 $.\/$ $/\$ $.\/$ $.\/$ $\/$ $.\/$
20	15, 19	sylib 196	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $\/$ $.\/$
21		simp3r2 1103	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
22		simp3l 1022	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
23		cdleme22.l	. . . . . . . . 9
24	23, 5, 6	hlatlej1 35496	. . . . . . . 8 $/\$ $/\$ $.\/$
25	1, 3, 22, 24	syl3anc 1226	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
26		hllat 35485	. . . . . . . . 9
27	1, 26	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
28		eqid 2454	. . . . . . . . . 10
29	28, 6	atbase 35411	. . . . . . . . 9
30	2, 29	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
31	28, 6	atbase 35411	. . . . . . . . 9
32	3, 31	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
33	28, 5, 6	hlatjcl 35488	. . . . . . . . 9 $/\$ $/\$ $.\/$
34	1, 3, 22, 33	syl3anc 1226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
35	28, 23, 5	latjle12 15891	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
36	27, 30, 32, 34, 35	syl13anc 1228	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
37	21, 25, 36	mpbi2and 919	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
38	37	adantr 463	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
39		simp3r3 1104	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
40	39	adantr 463	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
41		simpr 459	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
42		simp21 1027	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
43		simp22 1028	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
44	28, 5, 6	hlatjcl 35488	. . . . . . . . 9 $/\$ $/\$ $.\/$
45	1, 42, 43, 44	syl3anc 1226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
46	28, 23, 5	latjle12 15891	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
47	27, 30, 32, 45, 46	syl13anc 1228	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
48	47	adantr 463	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
49	40, 41, 48	mpbi2and 919	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
50	28, 5, 6	hlatjcl 35488	. . . . . . . 8 $/\$ $/\$ $.\/$
51	1, 2, 3, 50	syl3anc 1226	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
52		cdleme22.m	. . . . . . . 8 $./\$
53	28, 23, 52	latlem12 15907	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
54	27, 51, 34, 45, 53	syl13anc 1228	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
55	54	adantr 463	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
56	38, 49, 55	mpbi2and 919	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
57	56	ex 432	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
58		hlop 35484	. . . . . . . 8
59	1, 58	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
60	59	adantr 463	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
61	51	adantr 463	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
62		simprl 754	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
63		simprr 755	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
64	28, 23, 12, 6	leat3 35417	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $\/$ $.\/$
65	60, 61, 62, 63, 64	syl31anc 1229	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $\/$ $.\/$
66	65	exp32 603	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $\/$ $.\/$
67		breq2 4443	. . . . . . . . 9 $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
68	67	biimpa 482	. . . . . . . 8 $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
69	28, 23, 12	ople0 35309	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $.\/$
70	59, 51, 69	syl2anc 659	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
71	68, 70	syl5ib 219	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
72	71	imp 427	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
73	72	olcd 391	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $\/$ $.\/$
74	73	exp32 603	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $\/$ $.\/$
75		simp3r1 1102	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
76	5, 52, 12, 6	2atmat0 35647	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $\/$ $.\/$ $./\$ $.\/$
77	1, 3, 22, 42, 43, 75, 76	syl33anc 1241	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $\/$ $.\/$ $./\$ $.\/$
78	66, 74, 77	mpjaod 379	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $\/$ $.\/$
79	57, 78	syld 44	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $\/$ $.\/$
80	20, 79	mtod 177	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367 $/\$ w3a 971

wceq 1398

wcel 1823

wne 2649 class class class wbr 4439

cfv 5570 (class class class)co 6270

cbs 14716

cple 14791

cjn 15772

cmee 15773

cp0 15866

clat 15874

cops 35294

catm 35385

chlt 35472

clln 35612

clh 36105

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-ral 2809 df-rex 2810 df-reu 2811 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-op 4023 df-uni 4236 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-id 4784 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-riota 6232 df-ov 6273 df-oprab 6274 df-preset 15756 df-poset 15774 df-plt 15787 df-lub 15803 df-glb 15804 df-join 15805 df-meet 15806 df-p0 15868 df-p1 15869 df-lat 15875 df-clat 15937 df-oposet 35298 df-ol 35300 df-oml 35301 df-covers 35388 df-ats 35389 df-atl 35420 df-cvlat 35444 df-hlat 35473 df-llines 35619

This theorem is referenced by: cdleme22cN 36465 cdleme27a 36490

W3C validator