Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > con4biddc | Unicode version |
Description: A contraposition deduction. (Contributed by Jim Kingdon, 18-May-2018.) |
Ref | Expression |
---|---|
con4biddc.1 | DECID DECID |
Ref | Expression |
---|---|
con4biddc | DECID DECID |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con4biddc.1 | . . . . . 6 DECID DECID | |
2 | bi2 121 | . . . . . 6 | |
3 | 1, 2 | syl8 65 | . . . . 5 DECID DECID |
4 | condc 749 | . . . . . 6 DECID | |
5 | 4 | a2i 11 | . . . . 5 DECID DECID |
6 | 3, 5 | syl6 29 | . . . 4 DECID DECID |
7 | 6 | imp31 243 | . . 3 DECID DECID |
8 | bi1 111 | . . . . . 6 | |
9 | 1, 8 | syl8 65 | . . . . 5 DECID DECID |
10 | condc 749 | . . . . . 6 DECID | |
11 | 10 | imim2d 48 | . . . . 5 DECID DECID DECID |
12 | 9, 11 | sylcom 25 | . . . 4 DECID DECID |
13 | 12 | imp31 243 | . . 3 DECID DECID |
14 | 7, 13 | impbid 120 | . 2 DECID DECID |
15 | 14 | exp31 346 | 1 DECID DECID |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wa 97 wb 98 DECID wdc 742 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in2 545 ax-io 630 |
This theorem depends on definitions: df-bi 110 df-dc 743 |
This theorem is referenced by: necon4abiddc 2278 |
Copyright terms: Public domain | W3C validator |