ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dcan Unicode 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  ph  ->  (DECID  ps 
-> DECID  ( ph  /\  ps )
) )

Proof of Theorem dcan
StepHypRef Expression
1 simpl 108 . . . . . 6  |-  ( ( -.  ph  /\  ps )  ->  -.  ph )
21intnanrd 900 . . . . 5  |-  ( ( -.  ph  /\  ps )  ->  -.  ( ph  /\  ps ) )
32orim2i 733 . . . 4  |-  ( ( ( ph  /\  ps )  \/  ( -.  ph 
/\  ps ) )  -> 
( ( ph  /\  ps )  \/  -.  ( ph  /\  ps )
) )
4 simpr 109 . . . . . 6  |-  ( ( ( ph  \/  -.  ph )  /\  -.  ps )  ->  -.  ps )
54intnand 899 . . . . 5  |-  ( ( ( ph  \/  -.  ph )  /\  -.  ps )  ->  -.  ( ph  /\ 
ps ) )
65olcd 706 . . . 4  |-  ( ( ( ph  \/  -.  ph )  /\  -.  ps )  ->  ( ( ph  /\ 
ps )  \/  -.  ( ph  /\  ps )
) )
73, 6jaoi 688 . . 3  |-  ( ( ( ( ph  /\  ps )  \/  ( -.  ph  /\  ps )
)  \/  ( (
ph  \/  -.  ph )  /\  -.  ps ) )  ->  ( ( ph  /\ 
ps )  \/  -.  ( ph  /\  ps )
) )
8 df-dc 803 . . . . 5  |-  (DECID  ph  <->  ( ph  \/  -.  ph ) )
9 df-dc 803 . . . . 5  |-  (DECID  ps  <->  ( ps  \/  -.  ps ) )
108, 9anbi12i 453 . . . 4  |-  ( (DECID  ph  /\ DECID  ps ) 
<->  ( ( ph  \/  -.  ph )  /\  ( ps  \/  -.  ps )
) )
11 andi 790 . . . 4  |-  ( ( ( ph  \/  -.  ph )  /\  ( ps  \/  -.  ps )
)  <->  ( ( (
ph  \/  -.  ph )  /\  ps )  \/  (
( ph  \/  -.  ph )  /\  -.  ps ) ) )
12 andir 791 . . . . 5  |-  ( ( ( ph  \/  -.  ph )  /\  ps )  <->  ( ( ph  /\  ps )  \/  ( -.  ph 
/\  ps ) ) )
1312orbi1i 735 . . . 4  |-  ( ( ( ( ph  \/  -.  ph )  /\  ps )  \/  ( ( ph  \/  -.  ph )  /\  -.  ps ) )  <-> 
( ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ps )
)  \/  ( (
ph  \/  -.  ph )  /\  -.  ps ) ) )
1410, 11, 133bitri 205 . . 3  |-  ( (DECID  ph  /\ DECID  ps ) 
<->  ( ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ps )
)  \/  ( (
ph  \/  -.  ph )  /\  -.  ps ) ) )
15 df-dc 803 . . 3  |-  (DECID  ( ph  /\ 
ps )  <->  ( ( ph  /\  ps )  \/ 
-.  ( ph  /\  ps ) ) )
167, 14, 153imtr4i 200 . 2  |-  ( (DECID  ph  /\ DECID  ps )  -> DECID 
( ph  /\  ps )
)
1716ex 114 1  |-  (DECID  ph  ->  (DECID  ps 
-> DECID  ( ph  /\  ps )
) )
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  9081  gcdmndc  11533  gcdsupex  11542  gcdsupcl  11543  gcdaddm  11568  lcmval  11640  lcmcllem  11644  lcmledvds  11647  ctiunctlemudc  11845  nninfsellemdc  13008
  Copyright terms: Public domain W3C validator