dalem20 - Mathbox for Norm Megill

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

Theorem dalem20 33177

Description: Lemma for dath 33220. Show that a second dummy atom

exists outside of the

and

planes (when those planes are equal). (Contributed by NM, 14-Aug-2012.)

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

**Assertion**
Ref	Expression
dalem20	$/\$

Distinct variable groups:

$.\/$ ,

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

) $.\/$ (

)

(

)

(

)

(

)

**Proof of Theorem dalem20**
Step	Hyp	Ref	Expression
1		dalem.ph	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		dalem.l	. . . . 5
3		dalem.j	. . . . 5 $.\/$
4		dalem.a	. . . . 5
5		dalem20.y	. . . . 5 $.\/$ $.\/$
6	1, 2, 3, 4, 5	dalem18 33165	. . . 4
7	6	adantr 465	. . 3 $/\$
8		dalem20.o	. . . . . . 7
9		dalem20.z	. . . . . . 7 $.\/$ $.\/$
10	1, 2, 3, 4, 8, 5, 9	dalem19 33166	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
11	10	ex 434	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$
12	11	ancld 553	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
13	12	reximdva 2823	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$
14	7, 13	mpd 15	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$
15		dalem.ps	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
16		3anass 969	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
17	15, 16	bitri 249	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
18	17	2exbii 1635	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
19		r2ex 2748	. . 3 $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
20		r19.42v 2870	. . . 4 $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
21	20	rexbii 2735	. . 3 $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
22	18, 19, 21	3bitr2ri 274	. 2 $/\$ $/\$ $/\$ $.\/$
23	14, 22	sylib 196	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wex 1586

wcel 1756

wne 2601

wrex 2711 class class class wbr 4287

cfv 5413 (class class class)co 6086

cbs 14166

cple 14237

cjn 15106

catm 32748

chlt 32835

clpl 32976

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-ral 2715 df-rex 2716 df-reu 2717 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-op 3879 df-uni 4087 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-id 4631 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-riota 6047 df-ov 6089 df-oprab 6090 df-poset 15108 df-plt 15120 df-lub 15136 df-glb 15137 df-join 15138 df-meet 15139 df-p0 15201 df-p1 15202 df-lat 15208 df-clat 15270 df-oposet 32661 df-ol 32663 df-oml 32664 df-covers 32751 df-ats 32752 df-atl 32783 df-cvlat 32807 df-hlat 32836 df-llines 32982 df-lplanes 32983

This theorem is referenced by: dalem62 33218

W3C validator