sbthlem2 - Intuitionistic Logic Explorer

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

Theorem sbthlem2 6935

Description: Lemma for isbth 6944. (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 6934	. . . . . . . 8 $\$ $\$
4		imass2 4987	. . . . . . . 8 $\$ $\$ $\$ $\$
5		sscon 3261	. . . . . . . 8 $\$ $\$ $\$ $\$ $\$ $\$
6	3, 4, 5	mp2b 8	. . . . . . 7 $\$ $\$ $\$ $\$
7		imass2 4987	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
8		sscon 3261	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
9	6, 7, 8	mp2b 8	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$
10		imassrn 4964	. . . . . . . 8 $\$ $\$ $\$
11		sstr2 3154	. . . . . . . 8 $\$ $\$ $\$ $\$ $\$ $\$
12	10, 11	ax-mp 5	. . . . . . 7 $\$ $\$ $\$
13		difss 3253	. . . . . . 7 $\$ $\$
14		ssconb 3260	. . . . . . 7 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
15	12, 13, 14	sylancl 411	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
16	9, 15	mpbiri 167	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
17	16, 13	jctil 310	. . . 4 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
18	1, 13	ssexi 4127	. . . . 5 $\$ $\$
19		sseq1 3170	. . . . . 6 $\$ $\$ $\$ $\$
20		imaeq2 4949	. . . . . . . . 9 $\$ $\$ $\$ $\$
21	20	difeq2d 3245	. . . . . . . 8 $\$ $\$ $\$ $\$ $\$ $\$
22	21	imaeq2d 4953	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$
23		difeq2 3239	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$
24	22, 23	sseq12d 3178	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
25	19, 24	anbi12d 470	. . . . 5 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
26	18, 25	elab 2874	. . . 4 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
27	17, 26	sylibr 133	. . 3 $\$ $\$ $/\$ $\$ $\$
28	27, 2	eleqtrrdi 2264	. 2 $\$ $\$
29		elssuni 3824	. 2 $\$ $\$ $\$ $\$
30	28, 29	syl 14	1 $\$ $\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104

wceq 1348

wcel 2141

cab 2156

cvv 2730 $\$ cdif 3118

wss 3121

cuni 3796

crn 4612

cima 4614

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 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-14 2144 ax-ext 2152 ax-sep 4107 ax-pow 4160 ax-pr 4194

This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-rex 2454 df-rab 2457 df-v 2732 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-br 3990 df-opab 4051 df-xp 4617 df-cnv 4619 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624

This theorem is referenced by: sbthlemi3 6936

W3C validator