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

Theorem dn1dc 878
Description: DN1 for decidable propositions. Without the decidability conditions, DN1 can serve as a single axiom for Boolean algebra. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jim Kingdon, 22-Apr-2018.)
Assertion
Ref Expression
dn1dc  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  ->  ( -.  ( -.  ( -.  ( ph  \/  ps )  \/  ch )  \/  -.  ( ph  \/  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) ) )  <->  ch ) )

Proof of Theorem dn1dc
StepHypRef Expression
1 pm2.45 667 . . . . 5  |-  ( -.  ( ph  \/  ps )  ->  -.  ph )
2 imnan 634 . . . . 5  |-  ( ( -.  ( ph  \/  ps )  ->  -.  ph ) 
<->  -.  ( -.  ( ph  \/  ps )  /\  ph ) )
31, 2mpbi 137 . . . 4  |-  -.  ( -.  ( ph  \/  ps )  /\  ph )
43biorfi 675 . . 3  |-  ( ch  <->  ( ch  \/  ( -.  ( ph  \/  ps )  /\  ph ) ) )
5 orcom 657 . . 3  |-  ( ( ch  \/  ( -.  ( ph  \/  ps )  /\  ph ) )  <-> 
( ( -.  ( ph  \/  ps )  /\  ph )  \/  ch )
)
6 ordir 741 . . 3  |-  ( ( ( -.  ( ph  \/  ps )  /\  ph )  \/  ch )  <->  ( ( -.  ( ph  \/  ps )  \/  ch )  /\  ( ph  \/  ch ) ) )
74, 5, 63bitri 199 . 2  |-  ( ch  <->  ( ( -.  ( ph  \/  ps )  \/  ch )  /\  ( ph  \/  ch ) ) )
8 pm4.45 708 . . . . . 6  |-  ( ch  <->  ( ch  /\  ( ch  \/  th ) ) )
9 simprrl 499 . . . . . . 7  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  -> DECID  ch )
10 dcor 854 . . . . . . . . 9  |-  (DECID  ch  ->  (DECID  th 
-> DECID  ( ch  \/  th )
) )
1110imp 119 . . . . . . . 8  |-  ( (DECID  ch 
/\ DECID  th )  -> DECID  ( ch  \/  th ) )
1211ad2antll 468 . . . . . . 7  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  -> DECID  ( ch  \/  th ) )
13 anordc 874 . . . . . . 7  |-  (DECID  ch  ->  (DECID  ( ch  \/  th )  ->  ( ( ch  /\  ( ch  \/  th )
)  <->  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) ) ) )
149, 12, 13sylc 60 . . . . . 6  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  ->  (
( ch  /\  ( ch  \/  th ) )  <->  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) ) )
158, 14syl5bb 185 . . . . 5  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  ->  ( ch 
<->  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) ) )
1615orbi2d 714 . . . 4  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  ->  (
( ph  \/  ch ) 
<->  ( ph  \/  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) ) ) )
1716anbi2d 445 . . 3  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  ->  (
( ( -.  ( ph  \/  ps )  \/ 
ch )  /\  ( ph  \/  ch ) )  <-> 
( ( -.  ( ph  \/  ps )  \/ 
ch )  /\  ( ph  \/  -.  ( -. 
ch  \/  -.  ( ch  \/  th ) ) ) ) ) )
18 dcor 854 . . . . . . . 8  |-  (DECID  ph  ->  (DECID  ps 
-> DECID  ( ph  \/  ps )
) )
19 dcn 757 . . . . . . . 8  |-  (DECID  ( ph  \/  ps )  -> DECID  -.  ( ph  \/  ps ) )
2018, 19syl6 33 . . . . . . 7  |-  (DECID  ph  ->  (DECID  ps 
-> DECID  -.  ( ph  \/  ps ) ) )
2120imp 119 . . . . . 6  |-  ( (DECID  ph  /\ DECID  ps )  -> DECID  -.  ( ph  \/  ps ) )
2221adantrr 456 . . . . 5  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  -> DECID  -.  ( ph  \/  ps ) )
23 dcor 854 . . . . 5  |-  (DECID  -.  ( ph  \/  ps )  -> 
(DECID 
ch  -> DECID 
( -.  ( ph  \/  ps )  \/  ch ) ) )
2422, 9, 23sylc 60 . . . 4  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  -> DECID  ( -.  ( ph  \/  ps )  \/  ch ) )
25 dcn 757 . . . . . . . 8  |-  (DECID  ch  -> DECID  -.  ch )
269, 25syl 14 . . . . . . 7  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  -> DECID  -.  ch )
27 dcn 757 . . . . . . . 8  |-  (DECID  ( ch  \/  th )  -> DECID  -.  ( ch  \/  th )
)
2812, 27syl 14 . . . . . . 7  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  -> DECID  -.  ( ch  \/  th ) )
29 dcor 854 . . . . . . 7  |-  (DECID  -.  ch  ->  (DECID  -.  ( ch  \/  th )  -> DECID  ( -.  ch  \/  -.  ( ch  \/  th ) ) ) )
3026, 28, 29sylc 60 . . . . . 6  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  -> DECID  ( -.  ch  \/  -.  ( ch  \/  th ) ) )
31 dcn 757 . . . . . 6  |-  (DECID  ( -. 
ch  \/  -.  ( ch  \/  th ) )  -> DECID  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) )
3230, 31syl 14 . . . . 5  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  -> DECID  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) )
33 dcor 854 . . . . . 6  |-  (DECID  ph  ->  (DECID  -.  ( -.  ch  \/  -.  ( ch  \/  th ) )  -> DECID  ( ph  \/  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) ) ) )
3433imp 119 . . . . 5  |-  ( (DECID  ph  /\ DECID  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) )  -> DECID  ( ph  \/  -.  ( -. 
ch  \/  -.  ( ch  \/  th ) ) ) )
3532, 34syldan 270 . . . 4  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  -> DECID  ( ph  \/  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) ) )
36 anordc 874 . . . 4  |-  (DECID  ( -.  ( ph  \/  ps )  \/  ch )  ->  (DECID  ( ph  \/  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) )  -> 
( ( ( -.  ( ph  \/  ps )  \/  ch )  /\  ( ph  \/  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) ) )  <->  -.  ( -.  ( -.  ( ph  \/  ps )  \/  ch )  \/  -.  ( ph  \/  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) ) ) ) ) )
3724, 35, 36sylc 60 . . 3  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  ->  (
( ( -.  ( ph  \/  ps )  \/ 
ch )  /\  ( ph  \/  -.  ( -. 
ch  \/  -.  ( ch  \/  th ) ) ) )  <->  -.  ( -.  ( -.  ( ph  \/  ps )  \/  ch )  \/  -.  ( ph  \/  -.  ( -. 
ch  \/  -.  ( ch  \/  th ) ) ) ) ) )
3817, 37bitrd 181 . 2  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  ->  (
( ( -.  ( ph  \/  ps )  \/ 
ch )  /\  ( ph  \/  ch ) )  <->  -.  ( -.  ( -.  ( ph  \/  ps )  \/  ch )  \/  -.  ( ph  \/  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) ) ) ) )
397, 38syl5rbb 186 1  |-  ( (DECID  ph  /\  (DECID  ps  /\  (DECID  ch  /\ DECID  th )
) )  ->  ( -.  ( -.  ( -.  ( ph  \/  ps )  \/  ch )  \/  -.  ( ph  \/  -.  ( -.  ch  \/  -.  ( ch  \/  th ) ) ) )  <->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 101    <-> wb 102    \/ wo 639  DECID wdc 753
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640
This theorem depends on definitions:  df-bi 114  df-dc 754
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator