sbthlem2 - Intuitionistic Logic Explorer

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

Theorem sbthlem2 7156

Description: Lemma for isbth 7165. (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 7155	. . . . . . . 8 $\$ $\$
4		imass2 5112	. . . . . . . 8 $\$ $\$ $\$ $\$
5		sscon 3341	. . . . . . . 8 $\$ $\$ $\$ $\$ $\$ $\$
6	3, 4, 5	mp2b 8	. . . . . . 7 $\$ $\$ $\$ $\$
7		imass2 5112	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
8		sscon 3341	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
9	6, 7, 8	mp2b 8	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$
10		imassrn 5087	. . . . . . . 8 $\$ $\$ $\$
11		sstr2 3234	. . . . . . . 8 $\$ $\$ $\$ $\$ $\$ $\$
12	10, 11	ax-mp 5	. . . . . . 7 $\$ $\$ $\$
13		difss 3333	. . . . . . 7 $\$ $\$
14		ssconb 3340	. . . . . . 7 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
15	12, 13, 14	sylancl 413	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
16	9, 15	mpbiri 168	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
17	16, 13	jctil 312	. . . 4 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
18	1, 13	ssexi 4227	. . . . 5 $\$ $\$
19		sseq1 3250	. . . . . 6 $\$ $\$ $\$ $\$
20		imaeq2 5072	. . . . . . . . 9 $\$ $\$ $\$ $\$
21	20	difeq2d 3325	. . . . . . . 8 $\$ $\$ $\$ $\$ $\$ $\$
22	21	imaeq2d 5076	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$
23		difeq2 3319	. . . . . . 7 $\$ $\$ $\$ $\$ $\$ $\$
24	22, 23	sseq12d 3258	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
25	19, 24	anbi12d 473	. . . . 5 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
26	18, 25	elab 2950	. . . 4 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
27	17, 26	sylibr 134	. . 3 $\$ $\$ $/\$ $\$ $\$
28	27, 2	eleqtrrdi 2325	. 2 $\$ $\$
29		elssuni 3921	. 2 $\$ $\$ $\$ $\$
30	28, 29	syl 14	1 $\$ $\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105

wceq 1397

wcel 2202

cab 2217

cvv 2802 $\$ cdif 3197

wss 3200

cuni 3893

crn 4726

cima 4728

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-14 2205 ax-ext 2213 ax-sep 4207 ax-pow 4264 ax-pr 4299

This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ral 2515 df-rex 2516 df-rab 2519 df-v 2804 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-br 4089 df-opab 4151 df-xp 4731 df-cnv 4733 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738

This theorem is referenced by: sbthlemi3 7157

W3C validator