3dim1 - Mathbox for Norm Megill

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

Theorem 3dim1 32833

Description: Construct a 3-dimensional volume (height-4 element) on top of a given atom

. (Contributed by NM, 25-Jul-2012.)

**Hypotheses**
Ref	Expression
3dim0.j	$.\/$
3dim0.l
3dim0.a

**Assertion**
Ref	Expression
3dim1	$/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$

Distinct variable groups:

$.\/$ ,

Allowed substitution hints:

(

)

Proof of Theorem 3dim1 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		3dim0.j	. . . 4 $.\/$
2		3dim0.l	. . . 4
3		3dim0.a	. . . 4
4	1, 2, 3	3dim0 32823	. . 3 $/\$ $.\/$ $/\$ $.\/$ $.\/$
5	4	adantr 462	. 2 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
6		simpl2 987	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$
7	1, 2, 3	3dimlem1 32824	. . . . . . . . . . . 12 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
8	7	3ad2antl3 1147	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
9	1, 2, 3	3dim1lem5 32832	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
10	6, 8, 9	syl2anc 656	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
11		simp13 1015	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
12		simp22 1017	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
13		simp23 1018	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
14	11, 12, 13	3jca 1163	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$
15	14	ad2antrr 720	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $/\$
16		simpll1 1022	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $/\$
17		simp21 1016	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
18		simp32 1020	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
19		simp33 1021	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
20	17, 18, 19	3jca 1163	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
21	20	ad2antrr 720	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
22		simplr 749	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$
23		simpr 458	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
24	1, 2, 3	3dimlem2 32825	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
25	16, 21, 22, 23, 24	syl112anc 1217	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
26	1, 2, 3	3dim1lem5 32832	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
27	15, 25, 26	syl2anc 656	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
28	11, 17, 13	3jca 1163	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$
29	28	ad2antrr 720	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$
30		simp1 983	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$
31	17, 12	jca 529	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
32		simp31 1019	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
33	32, 19	jca 529	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
34	30, 31, 33	3jca 1163	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
35	34	ad2antrr 720	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
36		simplrl 754	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37		simplrr 755	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
38		simpr 458	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
39	1, 2, 3	3dimlem3 32827	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
40	35, 36, 37, 38, 39	syl13anc 1215	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
41	1, 2, 3	3dim1lem5 32832	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
42	29, 40, 41	syl2anc 656	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
43	11, 17, 12	3jca 1163	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$
44	43	ad2antrr 720	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$
45		simpl1 986	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $/\$
46		simpl21 1061	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$
47		simpl22 1062	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$
48	46, 47	jca 529	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$
49		simpl31 1064	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$
50		simpl32 1065	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
51	49, 50	jca 529	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
52	45, 48, 51	3jca 1163	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
53	52	adantr 462	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
54		simplr 749	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
55		simpr 458	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
56	1, 2, 3	3dimlem4 32830	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
57	53, 54, 55, 56	syl3anc 1213	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
58	1, 2, 3	3dim1lem5 32832	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
59	44, 57, 58	syl2anc 656	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
60	42, 59	pm2.61dan 784	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
61	60	anassrs 643	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
62	27, 61	pm2.61dan 784	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
63	10, 62	pm2.61dane 2687	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
64	63	3exp 1181	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
65	64	3expd 1199	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
66	65	3exp 1181	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
67	66	imp43 592	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
68	67	imp3a 431	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
69	68	rexlimdvv 2845	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
70	69	rexlimdvva 2846	. 2 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
71	5, 70	mpd 15	1 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 960

wceq 1364

wcel 1761

wne 2604

wrex 2714 class class class wbr 4289

cfv 5415 (class class class)co 6090

cple 14241

cjn 15110

catm 32630

chlt 32717

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-ral 2718 df-rex 2719 df-reu 2720 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-op 3881 df-uni 4089 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-id 4632 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-riota 6049 df-ov 6093 df-oprab 6094 df-poset 15112 df-plt 15124 df-lub 15140 df-glb 15141 df-join 15142 df-meet 15143 df-p0 15205 df-p1 15206 df-lat 15212 df-clat 15274 df-oposet 32543 df-ol 32545 df-oml 32546 df-covers 32633 df-ats 32634 df-atl 32665 df-cvlat 32689 df-hlat 32718

This theorem is referenced by: 3dim2 32834 2dim 32836

W3C validator