Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > dcan | Unicode version |
Description: A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.) |
Ref | Expression |
---|---|
dcan | DECID DECID DECID |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 108 | . . . . . 6 | |
2 | 1 | intnanrd 902 | . . . . 5 |
3 | 2 | orim2i 735 | . . . 4 |
4 | simpr 109 | . . . . . 6 | |
5 | 4 | intnand 901 | . . . . 5 |
6 | 5 | olcd 708 | . . . 4 |
7 | 3, 6 | jaoi 690 | . . 3 |
8 | df-dc 805 | . . . . 5 DECID | |
9 | df-dc 805 | . . . . 5 DECID | |
10 | 8, 9 | anbi12i 455 | . . . 4 DECID DECID |
11 | andi 792 | . . . 4 | |
12 | andir 793 | . . . . 5 | |
13 | 12 | orbi1i 737 | . . . 4 |
14 | 10, 11, 13 | 3bitri 205 | . . 3 DECID DECID |
15 | df-dc 805 | . . 3 DECID | |
16 | 7, 14, 15 | 3imtr4i 200 | . 2 DECID DECID DECID |
17 | 16 | ex 114 | 1 DECID DECID DECID |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wa 103 wo 682 DECID wdc 804 |
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 588 ax-in2 589 ax-io 683 |
This theorem depends on definitions: df-bi 116 df-dc 805 |
This theorem is referenced by: dcbi 905 annimdc 906 pm4.55dc 907 orandc 908 anordc 925 xordidc 1362 nn0n0n1ge2b 9098 gcdmndc 11564 gcdsupex 11573 gcdsupcl 11574 gcdaddm 11599 lcmval 11671 lcmcllem 11675 lcmledvds 11678 ctiunctlemudc 11877 nninfsellemdc 13133 |
Copyright terms: Public domain | W3C validator |