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

Theorem dcan 903
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 902 . . . . 5  |-  ( ( -.  ph  /\  ps )  ->  -.  ( ph  /\  ps ) )
32orim2i 735 . . . 4  |-  ( ( ( ph  /\  ps )  \/  ( -.  ph 
/\  ps ) )  -> 
( ( ph  /\  ps )  \/  -.  ( ph  /\  ps )
) )
4 simpr 109 . . . . . 6  |-  ( ( ( ph  \/  -.  ph )  /\  -.  ps )  ->  -.  ps )
54intnand 901 . . . . 5  |-  ( ( ( ph  \/  -.  ph )  /\  -.  ps )  ->  -.  ( ph  /\ 
ps ) )
65olcd 708 . . . 4  |-  ( ( ( ph  \/  -.  ph )  /\  -.  ps )  ->  ( ( ph  /\ 
ps )  \/  -.  ( ph  /\  ps )
) )
73, 6jaoi 690 . . 3  |-  ( ( ( ( ph  /\  ps )  \/  ( -.  ph  /\  ps )
)  \/  ( (
ph  \/  -.  ph )  /\  -.  ps ) )  ->  ( ( ph  /\ 
ps )  \/  -.  ( ph  /\  ps )
) )
8 df-dc 805 . . . . 5  |-  (DECID  ph  <->  ( ph  \/  -.  ph ) )
9 df-dc 805 . . . . 5  |-  (DECID  ps  <->  ( ps  \/  -.  ps ) )
108, 9anbi12i 455 . . . 4  |-  ( (DECID  ph  /\ DECID  ps ) 
<->  ( ( ph  \/  -.  ph )  /\  ( ps  \/  -.  ps )
) )
11 andi 792 . . . 4  |-  ( ( ( ph  \/  -.  ph )  /\  ( ps  \/  -.  ps )
)  <->  ( ( (
ph  \/  -.  ph )  /\  ps )  \/  (
( ph  \/  -.  ph )  /\  -.  ps ) ) )
12 andir 793 . . . . 5  |-  ( ( ( ph  \/  -.  ph )  /\  ps )  <->  ( ( ph  /\  ps )  \/  ( -.  ph 
/\  ps ) ) )
1312orbi1i 737 . . . 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 805 . . 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 682  DECID wdc 804
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 588  ax-in2 589  ax-io 683
This theorem depends on definitions:  df-bi 116  df-dc 805
This theorem is referenced by:  dcbi  905  annimdc  906  pm4.55dc  907  orandc  908  anordc  925  xordidc  1362  nn0n0n1ge2b  9098  gcdmndc  11564  gcdsupex  11573  gcdsupcl  11574  gcdaddm  11599  lcmval  11671  lcmcllem  11675  lcmledvds  11678  ctiunctlemudc  11877  nninfsellemdc  13133
  Copyright terms: Public domain W3C validator