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

Theorem biassdc 1341
Description: Associative law for the biconditional, for decidable propositions.

The classical version (without the decidability conditions) is an axiom of system DS in Vladimir Lifschitz, "On calculational proofs", Annals of Pure and Applied Logic, 113:207-224, 2002, http://www.cs.utexas.edu/users/ai-lab/pub-view.php?PubID=26805, and, interestingly, was not included in Principia Mathematica but was apparently first noted by Jan Lukasiewicz circa 1923. (Contributed by Jim Kingdon, 4-May-2018.)

Assertion
Ref Expression
biassdc  |-  (DECID  ph  ->  (DECID  ps 
->  (DECID  ch  ->  ( (
( ph  <->  ps )  <->  ch )  <->  (
ph 
<->  ( ps  <->  ch )
) ) ) ) )

Proof of Theorem biassdc
StepHypRef Expression
1 df-dc 787 . . 3  |-  (DECID  ph  <->  ( ph  \/  -.  ph ) )
2 pm5.501 243 . . . . . . 7  |-  ( ph  ->  ( ps  <->  ( ph  <->  ps ) ) )
32bibi1d 232 . . . . . 6  |-  ( ph  ->  ( ( ps  <->  ch )  <->  ( ( ph  <->  ps )  <->  ch ) ) )
4 pm5.501 243 . . . . . 6  |-  ( ph  ->  ( ( ps  <->  ch )  <->  (
ph 
<->  ( ps  <->  ch )
) ) )
53, 4bitr3d 189 . . . . 5  |-  ( ph  ->  ( ( ( ph  <->  ps )  <->  ch )  <->  ( ph  <->  ( ps  <->  ch ) ) ) )
65a1d 22 . . . 4  |-  ( ph  ->  ( (DECID  ps  /\ DECID  ch )  ->  (
( ( ph  <->  ps )  <->  ch )  <->  ( ph  <->  ( ps  <->  ch ) ) ) ) )
7 nbbndc 1340 . . . . . . . . 9  |-  (DECID  ps  ->  (DECID  ch 
->  ( ( -.  ps  <->  ch )  <->  -.  ( ps  <->  ch ) ) ) )
87imp 123 . . . . . . . 8  |-  ( (DECID  ps 
/\ DECID  ch )  ->  ( ( -.  ps  <->  ch )  <->  -.  ( ps  <->  ch )
) )
98adantl 273 . . . . . . 7  |-  ( ( -.  ph  /\  (DECID  ps  /\ DECID  ch ) )  ->  (
( -.  ps  <->  ch )  <->  -.  ( ps  <->  ch )
) )
10 nbn2 654 . . . . . . . . 9  |-  ( -. 
ph  ->  ( -.  ps  <->  (
ph 
<->  ps ) ) )
1110bibi1d 232 . . . . . . . 8  |-  ( -. 
ph  ->  ( ( -. 
ps 
<->  ch )  <->  ( ( ph 
<->  ps )  <->  ch )
) )
1211adantr 272 . . . . . . 7  |-  ( ( -.  ph  /\  (DECID  ps  /\ DECID  ch ) )  ->  (
( -.  ps  <->  ch )  <->  ( ( ph  <->  ps )  <->  ch ) ) )
139, 12bitr3d 189 . . . . . 6  |-  ( ( -.  ph  /\  (DECID  ps  /\ DECID  ch ) )  ->  ( -.  ( ps  <->  ch )  <->  ( ( ph  <->  ps )  <->  ch ) ) )
14 nbn2 654 . . . . . . 7  |-  ( -. 
ph  ->  ( -.  ( ps 
<->  ch )  <->  ( ph  <->  ( ps  <->  ch ) ) ) )
1514adantr 272 . . . . . 6  |-  ( ( -.  ph  /\  (DECID  ps  /\ DECID  ch ) )  ->  ( -.  ( ps  <->  ch )  <->  (
ph 
<->  ( ps  <->  ch )
) ) )
1613, 15bitr3d 189 . . . . 5  |-  ( ( -.  ph  /\  (DECID  ps  /\ DECID  ch ) )  ->  (
( ( ph  <->  ps )  <->  ch )  <->  ( ph  <->  ( ps  <->  ch ) ) ) )
1716ex 114 . . . 4  |-  ( -. 
ph  ->  ( (DECID  ps  /\ DECID  ch )  ->  ( ( ( ph  <->  ps )  <->  ch )  <->  ( ph  <->  ( ps  <->  ch ) ) ) ) )
186, 17jaoi 677 . . 3  |-  ( (
ph  \/  -.  ph )  ->  ( (DECID  ps  /\ DECID  ch )  ->  (
( ( ph  <->  ps )  <->  ch )  <->  ( ph  <->  ( ps  <->  ch ) ) ) ) )
191, 18sylbi 120 . 2  |-  (DECID  ph  ->  ( (DECID  ps  /\ DECID  ch )  ->  (
( ( ph  <->  ps )  <->  ch )  <->  ( ph  <->  ( ps  <->  ch ) ) ) ) )
2019expd 256 1  |-  (DECID  ph  ->  (DECID  ps 
->  (DECID  ch  ->  ( (
( ph  <->  ps )  <->  ch )  <->  (
ph 
<->  ( ps  <->  ch )
) ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 670  DECID wdc 786
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671
This theorem depends on definitions:  df-bi 116  df-dc 787
This theorem is referenced by:  bilukdc  1342
  Copyright terms: Public domain W3C validator