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 33170

Description: Lemma for dath 33213. 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 33158	. . . 4
7	6	adantr 466	. . 3 $/\$
8		dalem20.o	. . . . . . 7
9		dalem20.z	. . . . . . 7 $.\/$ $.\/$
10	1, 2, 3, 4, 8, 5, 9	dalem19 33159	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
11	10	ex 435	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$
12	11	ancld 555	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
13	12	reximdva 2839	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$
14	7, 13	mpd 15	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$
15		dalem.ps	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
16		3anass 986	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
17	15, 16	bitri 252	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
18	17	2exbii 1713	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
19		r2ex 2890	. . 3 $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
20		r19.42v 2922	. . . 4 $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
21	20	rexbii 2866	. . 3 $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
22	18, 19, 21	3bitr2ri 277	. 2 $/\$ $/\$ $/\$ $.\/$
23	14, 22	sylib 199	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1437

wex 1657

wcel 1872

wne 2599

wrex 2715 class class class wbr 4366

cfv 5544 (class class class)co 6249

cbs 15064

cple 15140

cjn 16132

catm 32741

chlt 32828

clpl 32969

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 2063 ax-ext 2408 ax-rep 4479 ax-sep 4489 ax-nul 4498 ax-pow 4545 ax-pr 4603 ax-un 6541

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 2280 df-mo 2281 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2558 df-ne 2601 df-ral 2719 df-rex 2720 df-reu 2721 df-rab 2723 df-v 3024 df-sbc 3243 df-csb 3339 df-dif 3382 df-un 3384 df-in 3386 df-ss 3393 df-nul 3705 df-if 3855 df-pw 3926 df-sn 3942 df-pr 3944 df-op 3948 df-uni 4163 df-iun 4244 df-br 4367 df-opab 4426 df-mpt 4427 df-id 4711 df-xp 4802 df-rel 4803 df-cnv 4804 df-co 4805 df-dm 4806 df-rn 4807 df-res 4808 df-ima 4809 df-iota 5508 df-fun 5546 df-fn 5547 df-f 5548 df-f1 5549 df-fo 5550 df-f1o 5551 df-fv 5552 df-riota 6211 df-ov 6252 df-oprab 6253 df-preset 16116 df-poset 16134 df-plt 16147 df-lub 16163 df-glb 16164 df-join 16165 df-meet 16166 df-p0 16228 df-p1 16229 df-lat 16235 df-clat 16297 df-oposet 32654 df-ol 32656 df-oml 32657 df-covers 32744 df-ats 32745 df-atl 32776 df-cvlat 32800 df-hlat 32829 df-llines 32975 df-lplanes 32976

This theorem is referenced by: dalem62 33211

W3C validator