Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sbcof2 | Unicode version |
Description: Version of sbco 1883 where is not free in . (Contributed by Jim Kingdon, 28-Dec-2017.) |
Ref | Expression |
---|---|
sbcof2.1 |
Ref | Expression |
---|---|
sbcof2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcof2.1 | . . . . . . 7 | |
2 | 1 | hbsb3 1729 | . . . . . 6 |
3 | 2 | sb6f 1724 | . . . . 5 |
4 | 1 | sb6f 1724 | . . . . . . 7 |
5 | 4 | imbi2i 224 | . . . . . 6 |
6 | 5 | albii 1399 | . . . . 5 |
7 | 3, 6 | bitri 182 | . . . 4 |
8 | ax-11 1437 | . . . . . . 7 | |
9 | equcomi 1632 | . . . . . . . . . . 11 | |
10 | 9 | imim1i 59 | . . . . . . . . . 10 |
11 | 10 | imim2i 12 | . . . . . . . . 9 |
12 | 11 | pm2.43d 49 | . . . . . . . 8 |
13 | 12 | alimi 1384 | . . . . . . 7 |
14 | 8, 13 | syl6 33 | . . . . . 6 |
15 | 14 | a2i 11 | . . . . 5 |
16 | 15 | alimi 1384 | . . . 4 |
17 | 7, 16 | sylbi 119 | . . 3 |
18 | ax-i9 1463 | . . . . 5 | |
19 | exim 1530 | . . . . 5 | |
20 | 18, 19 | mpi 15 | . . . 4 |
21 | ax-ial 1467 | . . . . 5 | |
22 | 21 | 19.9h 1574 | . . . 4 |
23 | 20, 22 | sylib 120 | . . 3 |
24 | sb2 1690 | . . 3 | |
25 | 17, 23, 24 | 3syl 17 | . 2 |
26 | sb1 1689 | . . . 4 | |
27 | simpl 107 | . . . . . 6 | |
28 | 19.8a 1522 | . . . . . 6 | |
29 | 27, 28 | jca 300 | . . . . 5 |
30 | 29 | eximi 1531 | . . . 4 |
31 | 9 | anim1i 333 | . . . . . . . . 9 |
32 | 27, 31 | jca 300 | . . . . . . . 8 |
33 | 32 | eximi 1531 | . . . . . . 7 |
34 | ax11e 1717 | . . . . . . 7 | |
35 | 33, 34 | syl5 32 | . . . . . 6 |
36 | 35 | imdistani 433 | . . . . 5 |
37 | 36 | eximi 1531 | . . . 4 |
38 | 26, 30, 37 | 3syl 17 | . . 3 |
39 | 2 | sb5f 1725 | . . . 4 |
40 | 1 | sb5f 1725 | . . . . . 6 |
41 | 40 | anbi2i 444 | . . . . 5 |
42 | 41 | exbii 1536 | . . . 4 |
43 | 39, 42 | bitri 182 | . . 3 |
44 | 38, 43 | sylibr 132 | . 2 |
45 | 25, 44 | impbii 124 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 wb 103 wal 1282 wex 1421 wsb 1685 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-11 1437 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 |
This theorem depends on definitions: df-bi 115 df-sb 1686 |
This theorem is referenced by: sbid2h 1770 |
Copyright terms: Public domain | W3C validator |