Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  dcim Unicode version

Theorem dcim 826
 Description: An implication between two decidable propositions is decidable. (Contributed by Jim Kingdon, 28-Mar-2018.)
Assertion
Ref Expression
dcim DECID DECID DECID

Proof of Theorem dcim
StepHypRef Expression
1 df-dc 820 . 2 DECID
2 df-dc 820 . . . . . . . 8 DECID
32anbi2i 452 . . . . . . 7 DECID
4 andi 807 . . . . . . 7
53, 4bitri 183 . . . . . 6 DECID
6 pm3.4 331 . . . . . . 7
7 annimim 675 . . . . . . 7
86, 7orim12i 748 . . . . . 6
95, 8sylbi 120 . . . . 5 DECID
10 df-dc 820 . . . . 5 DECID
119, 10sylibr 133 . . . 4 DECID DECID
1211ex 114 . . 3 DECID DECID
13 ax-in2 604 . . . . 5
1413a1d 22 . . . 4 DECID
15 orc 701 . . . . 5
1615, 10sylibr 133 . . . 4 DECID
1714, 16syl6 33 . . 3 DECID DECID
1812, 17jaoi 705 . 2 DECID DECID
191, 18sylbi 120 1 DECID DECID DECID
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wo 697  DECID wdc 819 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 603  ax-in2 604  ax-io 698 This theorem depends on definitions:  df-bi 116  df-dc 820 This theorem is referenced by:  pm4.79dc  888  pm5.11dc  894  dcbi  920  annimdc  921
 Copyright terms: Public domain W3C validator