cdlemefrs29cpre1 - Mathbox for Norm Megill

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

Theorem cdlemefrs29cpre1 33934

Description: TODO FIX COMMENT (Contributed by NM, 29-Mar-2013.)

**Hypotheses**
Ref	Expression
cdlemefrs27.b
cdlemefrs27.l
cdlemefrs27.j	$.\/$
cdlemefrs27.m	$./\$
cdlemefrs27.a
cdlemefrs27.h
cdlemefrs27.eq
cdlemefrs27.nb	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
cdlemefrs27.rnb	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

Distinct variable groups:

$.\/$ ,

, $.\/$ $./\$ ,

Allowed substitution hints:

(

)

(

)

**Proof of Theorem cdlemefrs29cpre1**
Step	Hyp	Ref	Expression
1		cdlemefrs27.b	. . 3
2		cdlemefrs27.l	. . 3
3		cdlemefrs27.j	. . 3 $.\/$
4		cdlemefrs27.m	. . 3 $./\$
5		cdlemefrs27.a	. . 3
6		cdlemefrs27.h	. . 3
7		cdlemefrs27.eq	. . 3
8		cdlemefrs27.nb	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9		cdlemefrs27.rnb	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10	1, 2, 3, 4, 5, 6, 7, 8, 9	cdlemefrs29bpre1 33933	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
11		simp11 1035	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		simp2rl 1074	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13	1, 5	atbase 32824	. . . . . 6
14	12, 13	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simp2rr 1075	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16	1, 2, 3, 4, 5, 6	lhpmcvr2 33558	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
17	11, 14, 15, 16	syl12anc 1262	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
18		simpl3 1010	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19	7	pm5.32ri 642	. . . . . . . . . 10 $/\$ $/\$
20	19	baibr 912	. . . . . . . . 9 $/\$
21	18, 20	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		simp2r 1032	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
23		eqid 2422	. . . . . . . . . . . . . 14
24	2, 4, 23, 5, 6	lhpmat 33564	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $./\$
25	11, 22, 24	syl2anc 665	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
26	25	adantr 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
27	26	oveq2d 6321	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
28		simp11l 1116	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29		hlol 32896	. . . . . . . . . . . 12
30	28, 29	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31	1, 5	atbase 32824	. . . . . . . . . . 11
32	1, 3, 23	olj01 32760	. . . . . . . . . . 11 $/\$ $.\/$
33	30, 31, 32	syl2an 479	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
34	27, 33	eqtrd 2463	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
35	34	eqeq1d 2424	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
36	35	anbi2d 708	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
37	21, 35, 36	3bitr4d 288	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
38	37	anbi2d 708	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$
39		anass 653	. . . . . 6 $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$
40	38, 39	syl6bbr 266	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$
41	40	rexbidva 2933	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$
42	17, 41	mpbid 213	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
43		reusv1 4624	. . 3 $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
44	42, 43	syl 17	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
45	10, 44	mpbird 235	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1872

wne 2614

wral 2771

wrex 2772

wreu 2773

csb 3395 class class class wbr 4423

cfv 5601 (class class class)co 6305

cbs 15120

cple 15196

cjn 16188

cmee 16189

cp0 16282

col 32709

catm 32798

chlt 32885

clh 33518

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-ral 2776 df-rex 2777 df-reu 2778 df-rmo 2779 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-op 4005 df-uni 4220 df-iun 4301 df-br 4424 df-opab 4483 df-mpt 4484 df-id 4768 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6267 df-ov 6308 df-oprab 6309 df-preset 16172 df-poset 16190 df-plt 16203 df-lub 16219 df-glb 16220 df-join 16221 df-meet 16222 df-p0 16284 df-p1 16285 df-lat 16291 df-clat 16353 df-oposet 32711 df-ol 32713 df-oml 32714 df-covers 32801 df-ats 32802 df-atl 32833 df-cvlat 32857 df-hlat 32886 df-lhyp 33522

This theorem is referenced by: cdlemefrs29clN 33935 cdlemefrs32fva 33936 cdlemefs29cpre1N 33954

W3C validator