![]() |
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 6982 nn0n0n1ge2b 9334 gcdmndc 11947 gcdsupex 11960 gcdsupcl 11961 gcdaddm 11987 nnwosdc 12042 lcmval 12065 lcmcllem 12069 lcmledvds 12072 prmdc 12132 pclemdc 12290 pcmptdvds 12345 infpnlem2 12360 1arith 12367 ctiunctlemudc 12440 nninfdclemcl 12451 nninfdclemp1 12453 lgsval 14444 lgscllem 14447 lgsneg 14464 lgsdir 14475 lgsdi 14477 lgsne0 14478 nninfsellemdc 14798 |
Copyright terms: Public domain | W3C validator |