sbthlem2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > sbthlem2		Unicode version

Theorem sbthlem2 6923

Description: Lemma for isbth 6932. (Contributed by NM, 22-Mar-1998.)

**Hypotheses**
Ref	Expression
sbthlem.1
sbthlem.2	$/\$ $\$ $\$

**Assertion**
Ref	Expression
sbthlem2	$\$ $\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem sbthlem2**
Step	Hyp	Ref	Expression
1		sbthlem.1	. . . . . . . . 9
2		sbthlem.2	. . . . . . . . 9 $/\$ $\$ $\$
3	1, 2	sbthlem1 6922	. . . . . . . 8 $\$ $\$
4		imass2 4980	. . . . . . . 8 $\$ $\$ $\$ $\$
5		sscon 3256	. . . . . . . 8 $\$ $\$ $\$ $\$ $\$ $\$
6	3, 4, 5	mp2b 8	. . . . . . 7 $\$ $\$ $\$ $\$
7		imass2 4980	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
8		sscon 3256	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
9	6, 7, 8	mp2b 8	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$
10		imassrn 4957	. . . . . . . 8 $\$ $\$ $\$
11		sstr2 3149	. . . . . . . 8 $\$ $\$ $\$ $\$ $\$ $\$
12	10, 11	ax-mp 5	. . . . . . 7 $\$ $\$ $\$
13		difss 3248	. . . . . . 7 $\$ $\$
14		ssconb 3255	. . . . . . 7 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
15	12, 13, 14	sylancl 410	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
16	9, 15	mpbiri 167	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
17	16, 13	jctil 310	. . . 4 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
18	1, 13	ssexi 4120	. . . . 5 $\$ $\$
19		sseq1 3165	. . . . . 6 $\$ $\$ $\$ $\$
20		imaeq2 4942	. . . . . . . . 9 $\$ $\$ $\$ $\$
21	20	difeq2d 3240	. . . . . . . 8 $\$ $\$ $\$ $\$ $\$ $\$
22	21	imaeq2d 4946	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$
23		difeq2 3234	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$
24	22, 23	sseq12d 3173	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
25	19, 24	anbi12d 465	. . . . 5 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
26	18, 25	elab 2870	. . . 4 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
27	17, 26	sylibr 133	. . 3 $\$ $\$ $/\$ $\$ $\$
28	27, 2	eleqtrrdi 2260	. 2 $\$ $\$
29		elssuni 3817	. 2 $\$ $\$ $\$ $\$
30	28, 29	syl 14	1 $\$ $\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104

wceq 1343

wcel 2136

cab 2151

cvv 2726 $\$ cdif 3113

wss 3116

cuni 3789

crn 4605

cima 4607

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-14 2139 ax-ext 2147 ax-sep 4100 ax-pow 4153 ax-pr 4187

This theorem depends on definitions: df-bi 116 df-3an 970 df-tru 1346 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ral 2449 df-rex 2450 df-rab 2453 df-v 2728 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-br 3983 df-opab 4044 df-xp 4610 df-cnv 4612 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617

This theorem is referenced by: sbthlemi3 6924

W3C validator