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

Theorem dcan 880
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 107 . . . . . 6  |-  ( ( -.  ph  /\  ps )  ->  -.  ph )
21intnanrd 879 . . . . 5  |-  ( ( -.  ph  /\  ps )  ->  -.  ( ph  /\  ps ) )
32orim2i 713 . . . 4  |-  ( ( ( ph  /\  ps )  \/  ( -.  ph 
/\  ps ) )  -> 
( ( ph  /\  ps )  \/  -.  ( ph  /\  ps )
) )
4 simpr 108 . . . . . 6  |-  ( ( ( ph  \/  -.  ph )  /\  -.  ps )  ->  -.  ps )
54intnand 878 . . . . 5  |-  ( ( ( ph  \/  -.  ph )  /\  -.  ps )  ->  -.  ( ph  /\ 
ps ) )
65olcd 688 . . . 4  |-  ( ( ( ph  \/  -.  ph )  /\  -.  ps )  ->  ( ( ph  /\ 
ps )  \/  -.  ( ph  /\  ps )
) )
73, 6jaoi 671 . . 3  |-  ( ( ( ( ph  /\  ps )  \/  ( -.  ph  /\  ps )
)  \/  ( (
ph  \/  -.  ph )  /\  -.  ps ) )  ->  ( ( ph  /\ 
ps )  \/  -.  ( ph  /\  ps )
) )
8 df-dc 781 . . . . 5  |-  (DECID  ph  <->  ( ph  \/  -.  ph ) )
9 df-dc 781 . . . . 5  |-  (DECID  ps  <->  ( ps  \/  -.  ps ) )
108, 9anbi12i 448 . . . 4  |-  ( (DECID  ph  /\ DECID  ps ) 
<->  ( ( ph  \/  -.  ph )  /\  ( ps  \/  -.  ps )
) )
11 andi 767 . . . 4  |-  ( ( ( ph  \/  -.  ph )  /\  ( ps  \/  -.  ps )
)  <->  ( ( (
ph  \/  -.  ph )  /\  ps )  \/  (
( ph  \/  -.  ph )  /\  -.  ps ) ) )
12 andir 768 . . . . 5  |-  ( ( ( ph  \/  -.  ph )  /\  ps )  <->  ( ( ph  /\  ps )  \/  ( -.  ph 
/\  ps ) ) )
1312orbi1i 715 . . . 4  |-  ( ( ( ( ph  \/  -.  ph )  /\  ps )  \/  ( ( ph  \/  -.  ph )  /\  -.  ps ) )  <-> 
( ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ps )
)  \/  ( (
ph  \/  -.  ph )  /\  -.  ps ) ) )
1410, 11, 133bitri 204 . . 3  |-  ( (DECID  ph  /\ DECID  ps ) 
<->  ( ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ps )
)  \/  ( (
ph  \/  -.  ph )  /\  -.  ps ) ) )
15 df-dc 781 . . 3  |-  (DECID  ( ph  /\ 
ps )  <->  ( ( ph  /\  ps )  \/ 
-.  ( ph  /\  ps ) ) )
167, 14, 153imtr4i 199 . 2  |-  ( (DECID  ph  /\ DECID  ps )  -> DECID 
( ph  /\  ps )
)
1716ex 113 1  |-  (DECID  ph  ->  (DECID  ps 
-> DECID  ( ph  /\  ps )
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    \/ wo 664  DECID wdc 780
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 579  ax-in2 580  ax-io 665
This theorem depends on definitions:  df-bi 115  df-dc 781
This theorem is referenced by:  dcbi  882  annimdc  883  pm4.55dc  884  orandc  885  anordc  902  xordidc  1335  nn0n0n1ge2b  8796  gcdmndc  11033  gcdsupex  11042  gcdsupcl  11043  gcdaddm  11068  lcmval  11138  lcmcllem  11142  lcmledvds  11145  nninfsellemdc  11559
  Copyright terms: Public domain W3C validator