![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dcan2 | Unicode version |
Description: A conjunction of two decidable propositions is decidable, expressed in a curried form as compared to dcan 933. (Contributed by Jim Kingdon, 12-Apr-2018.) |
Ref | Expression |
---|---|
dcan2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dcan 933 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 115 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 614 ax-in2 615 ax-io 709 |
This theorem depends on definitions: df-bi 117 df-dc 835 |
This theorem is referenced by: dcbi 936 annimdc 937 pm4.55dc 938 orandc 939 anordc 956 xordidc 1399 dcfi 6979 nn0n0n1ge2b 9331 gcdmndc 11944 gcdsupex 11957 gcdsupcl 11958 gcdaddm 11984 nnwosdc 12039 lcmval 12062 lcmcllem 12066 lcmledvds 12069 prmdc 12129 pclemdc 12287 pcmptdvds 12342 infpnlem2 12357 1arith 12364 ctiunctlemudc 12437 nninfdclemcl 12448 nninfdclemp1 12450 lgsval 14375 lgscllem 14378 lgsneg 14395 lgsdir 14406 lgsdi 14408 lgsne0 14409 nninfsellemdc 14729 |
Copyright terms: Public domain | W3C validator |