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

Theorem sbthlemi6 6860
 Description: Lemma for isbth 6865. (Contributed by NM, 27-Mar-1998.)
Hypotheses
Ref Expression
sbthlem.1
sbthlem.2
sbthlem.3
Assertion
Ref Expression
sbthlemi6 EXMID
Distinct variable groups:   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,)   (,)   (,)   (,)

Proof of Theorem sbthlemi6
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpll 519 . . 3 EXMID EXMID
2 simprll 527 . . 3 EXMID
3 simprlr 528 . . 3 EXMID
4 simprr 522 . . 3 EXMID
5 rnun 4956 . . . . 5
6 sbthlem.3 . . . . . 6
76rneqi 4776 . . . . 5
8 df-ima 4561 . . . . . 6
98uneq1i 3232 . . . . 5
105, 7, 93eqtr4i 2171 . . . 4
11 df-ima 4561 . . . . . 6
12 sbthlem.1 . . . . . . 7
13 sbthlem.2 . . . . . . 7
1412, 13sbthlemi4 6858 . . . . . 6 EXMID
1511, 14syl5reqr 2188 . . . . 5 EXMID
1615uneq2d 3236 . . . 4 EXMID
1710, 16eqtr4id 2192 . . 3 EXMID
181, 2, 3, 4, 17syl121anc 1222 . 2 EXMID
19 imassrn 4901 . . . . . . 7
20 sstr2 3110 . . . . . . 7
2119, 20ax-mp 5 . . . . . 6
2221adantl 275 . . . . 5 EXMID
23 undifdcss 6821 . . . . . . 7 DECID
24 exmidexmid 4129 . . . . . . . . 9 EXMID DECID
2524ralrimivw 2510 . . . . . . . 8 EXMID DECID
2625biantrud 302 . . . . . . 7 EXMID DECID
2723, 26bitr4id 198 . . . . . 6 EXMID
2827adantr 274 . . . . 5 EXMID
2922, 28mpbird 166 . . . 4 EXMID
3029eqcomd 2146 . . 3 EXMID