dalem31N - Mathbox for Norm Megill

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

Theorem dalem31N 32720

Description: Lemma for dath 32753. Analog of dalem25 32715 for

. (Contributed by NM, 4-Aug-2012.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
dalem.ph	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
dalem.l
dalem.j	$.\/$
dalem.a
dalem.ps	$/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
dalem29.m	$./\$
dalem29.o
dalem29.y	$.\/$ $.\/$
dalem29.z	$.\/$ $.\/$
dalem29.h	$.\/$ $./\$ $.\/$

**Assertion**
Ref	Expression
dalem31N	$/\$ $/\$

**Proof of Theorem dalem31N**
Step	Hyp	Ref	Expression
1		dalem.ph	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		dalem.l	. . . 4
3		dalem.j	. . . 4 $.\/$
4		dalem.a	. . . 4
5		dalem29.y	. . . 4 $.\/$ $.\/$
6		dalem29.z	. . . 4 $.\/$ $.\/$
7	1, 2, 3, 4, 5, 6	dalemrot 32674	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
8	7	3ad2ant1 1018	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
9	1, 2, 3, 4, 5, 6	dalemrotyz 32675	. . 3 $/\$ $.\/$ $.\/$ $.\/$ $.\/$
10	9	3adant3 1017	. 2 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
11		dalem.ps	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
12	1, 2, 3, 4, 11, 5	dalemrotps 32708	. . 3 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
13	12	3adant2 1016	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
14		biid 236	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
15		biid 236	. . 3 $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
16		dalem29.m	. . 3 $./\$
17		dalem29.o	. . 3
18		eqid 2402	. . 3 $.\/$ $.\/$ $.\/$ $.\/$
19		eqid 2402	. . 3 $.\/$ $.\/$ $.\/$ $.\/$
20		dalem29.h	. . 3 $.\/$ $./\$ $.\/$
21	14, 2, 3, 4, 15, 16, 17, 18, 19, 20	dalem25 32715	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
22	8, 10, 13, 21	syl3anc 1230	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842

wne 2598 class class class wbr 4395

cfv 5569 (class class class)co 6278

cbs 14841

cple 14916

cjn 15897

cmee 15898

catm 32281

chlt 32368

clpl 32509

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4507 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-ral 2759 df-rex 2760 df-reu 2761 df-rab 2763 df-v 3061 df-sbc 3278 df-csb 3374 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-nul 3739 df-if 3886 df-pw 3957 df-sn 3973 df-pr 3975 df-op 3979 df-uni 4192 df-iun 4273 df-br 4396 df-opab 4454 df-mpt 4455 df-id 4738 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-iota 5533 df-fun 5571 df-fn 5572 df-f 5573 df-f1 5574 df-fo 5575 df-f1o 5576 df-fv 5577 df-riota 6240 df-ov 6281 df-oprab 6282 df-preset 15881 df-poset 15899 df-plt 15912 df-lub 15928 df-glb 15929 df-join 15930 df-meet 15931 df-p0 15993 df-lat 16000 df-clat 16062 df-oposet 32194 df-ol 32196 df-oml 32197 df-covers 32284 df-ats 32285 df-atl 32316 df-cvlat 32340 df-hlat 32369 df-llines 32515 df-lplanes 32516

This theorem is referenced by: (None)

W3C validator