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

Theorem dcan 901
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 108 . . . . . 6 ((¬ 𝜑𝜓) → ¬ 𝜑)
21intnanrd 900 . . . . 5 ((¬ 𝜑𝜓) → ¬ (𝜑𝜓))
32orim2i 733 . . . 4 (((𝜑𝜓) ∨ (¬ 𝜑𝜓)) → ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
4 simpr 109 . . . . . 6 (((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓) → ¬ 𝜓)
54intnand 899 . . . . 5 (((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓) → ¬ (𝜑𝜓))
65olcd 706 . . . 4 (((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓) → ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
73, 6jaoi 688 . . 3 ((((𝜑𝜓) ∨ (¬ 𝜑𝜓)) ∨ ((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓)) → ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
8 df-dc 803 . . . . 5 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
9 df-dc 803 . . . . 5 (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
108, 9anbi12i 453 . . . 4 ((DECID 𝜑DECID 𝜓) ↔ ((𝜑 ∨ ¬ 𝜑) ∧ (𝜓 ∨ ¬ 𝜓)))
11 andi 790 . . . 4 (((𝜑 ∨ ¬ 𝜑) ∧ (𝜓 ∨ ¬ 𝜓)) ↔ (((𝜑 ∨ ¬ 𝜑) ∧ 𝜓) ∨ ((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓)))
12 andir 791 . . . . 5 (((𝜑 ∨ ¬ 𝜑) ∧ 𝜓) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜓)))
1312orbi1i 735 . . . 4 ((((𝜑 ∨ ¬ 𝜑) ∧ 𝜓) ∨ ((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓)) ↔ (((𝜑𝜓) ∨ (¬ 𝜑𝜓)) ∨ ((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓)))
1410, 11, 133bitri 205 . . 3 ((DECID 𝜑DECID 𝜓) ↔ (((𝜑𝜓) ∨ (¬ 𝜑𝜓)) ∨ ((𝜑 ∨ ¬ 𝜑) ∧ ¬ 𝜓)))
15 df-dc 803 . . 3 (DECID (𝜑𝜓) ↔ ((𝜑𝜓) ∨ ¬ (𝜑𝜓)))
167, 14, 153imtr4i 200 . 2 ((DECID 𝜑DECID 𝜓) → DECID (𝜑𝜓))
1716ex 114 1 (DECID 𝜑 → (DECID 𝜓DECID (𝜑𝜓)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wo 680  DECID wdc 802
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 586  ax-in2 587  ax-io 681
This theorem depends on definitions:  df-bi 116  df-dc 803
This theorem is referenced by:  dcbi  903  annimdc  904  pm4.55dc  905  orandc  906  anordc  923  xordidc  1360  nn0n0n1ge2b  9084  gcdmndc  11544  gcdsupex  11553  gcdsupcl  11554  gcdaddm  11579  lcmval  11651  lcmcllem  11655  lcmledvds  11658  ctiunctlemudc  11856  nninfsellemdc  13040
  Copyright terms: Public domain W3C validator