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

Theorem dcan 878
Description: A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
Assertion
Ref Expression
dcan (DECID 𝜑 → (DECID 𝜓DECID (𝜑𝜓)))

Proof of Theorem dcan
StepHypRef Expression
1 simpl 107 . . . . . 6 ((¬ 𝜑𝜓) → ¬ 𝜑)
21intnanrd 877 . . . . 5 ((¬ 𝜑𝜓) → ¬ (𝜑𝜓))
32orim2i 711 . . . 4 (((𝜑𝜓) ∨ (¬ 𝜑𝜓)) → ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
4 simpr 108 . . . . . 6 (((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓) → ¬ 𝜓)
54intnand 876 . . . . 5 (((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓) → ¬ (𝜑𝜓))
65olcd 686 . . . 4 (((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓) → ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
73, 6jaoi 669 . . 3 ((((𝜑𝜓) ∨ (¬ 𝜑𝜓)) ∨ ((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓)) → ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
8 df-dc 779 . . . . 5 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
9 df-dc 779 . . . . 5 (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
108, 9anbi12i 448 . . . 4 ((DECID 𝜑DECID 𝜓) ↔ ((𝜑 ∨ ¬ 𝜑) ∧ (𝜓 ∨ ¬ 𝜓)))
11 andi 765 . . . 4 (((𝜑 ∨ ¬ 𝜑) ∧ (𝜓 ∨ ¬ 𝜓)) ↔ (((𝜑 ∨ ¬ 𝜑) ∧ 𝜓) ∨ ((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓)))
12 andir 766 . . . . 5 (((𝜑 ∨ ¬ 𝜑) ∧ 𝜓) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜓)))
1312orbi1i 713 . . . 4 ((((𝜑 ∨ ¬ 𝜑) ∧ 𝜓) ∨ ((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓)) ↔ (((𝜑𝜓) ∨ (¬ 𝜑𝜓)) ∨ ((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓)))
1410, 11, 133bitri 204 . . 3 ((DECID 𝜑DECID 𝜓) ↔ (((𝜑𝜓) ∨ (¬ 𝜑𝜓)) ∨ ((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓)))
15 df-dc 779 . . 3 (DECID (𝜑𝜓) ↔ ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
167, 14, 153imtr4i 199 . 2 ((DECID 𝜑DECID 𝜓) → DECID (𝜑𝜓))
1716ex 113 1 (DECID 𝜑 → (DECID 𝜓DECID (𝜑𝜓)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wo 662  DECID wdc 778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663
This theorem depends on definitions:  df-bi 115  df-dc 779
This theorem is referenced by:  dcbi  880  annimdc  881  pm4.55dc  882  orandc  883  anordc  900  xordidc  1333  nn0n0n1ge2b  8759  gcdmndc  10822  gcdsupex  10831  gcdsupcl  10832  gcdaddm  10857  lcmval  10927  lcmcllem  10931  lcmledvds  10934  nninfsellemdc  11347
  Copyright terms: Public domain W3C validator