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

Theorem biassdc 1283
 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 φ → (DECID ψ → (DECID χ → (((φψ) ↔ χ) ↔ (φ ↔ (ψχ))))))

Proof of Theorem biassdc
StepHypRef Expression
1 df-dc 742 . . 3 (DECID φ ↔ (φ ¬ φ))
2 pm5.501 233 . . . . . . 7 (φ → (ψ ↔ (φψ)))
32bibi1d 222 . . . . . 6 (φ → ((ψχ) ↔ ((φψ) ↔ χ)))
4 pm5.501 233 . . . . . 6 (φ → ((ψχ) ↔ (φ ↔ (ψχ))))
53, 4bitr3d 179 . . . . 5 (φ → (((φψ) ↔ χ) ↔ (φ ↔ (ψχ))))
65a1d 22 . . . 4 (φ → ((DECID ψ DECID χ) → (((φψ) ↔ χ) ↔ (φ ↔ (ψχ)))))
7 nbbndc 1282 . . . . . . . . 9 (DECID ψ → (DECID χ → ((¬ ψχ) ↔ ¬ (ψχ))))
87imp 115 . . . . . . . 8 ((DECID ψ DECID χ) → ((¬ ψχ) ↔ ¬ (ψχ)))
98adantl 262 . . . . . . 7 ((¬ φ (DECID ψ DECID χ)) → ((¬ ψχ) ↔ ¬ (ψχ)))
10 nbn2 612 . . . . . . . . 9 φ → (¬ ψ ↔ (φψ)))
1110bibi1d 222 . . . . . . . 8 φ → ((¬ ψχ) ↔ ((φψ) ↔ χ)))
1211adantr 261 . . . . . . 7 ((¬ φ (DECID ψ DECID χ)) → ((¬ ψχ) ↔ ((φψ) ↔ χ)))
139, 12bitr3d 179 . . . . . 6 ((¬ φ (DECID ψ DECID χ)) → (¬ (ψχ) ↔ ((φψ) ↔ χ)))
14 nbn2 612 . . . . . . 7 φ → (¬ (ψχ) ↔ (φ ↔ (ψχ))))
1514adantr 261 . . . . . 6 ((¬ φ (DECID ψ DECID χ)) → (¬ (ψχ) ↔ (φ ↔ (ψχ))))
1613, 15bitr3d 179 . . . . 5 ((¬ φ (DECID ψ DECID χ)) → (((φψ) ↔ χ) ↔ (φ ↔ (ψχ))))
1716ex 108 . . . 4 φ → ((DECID ψ DECID χ) → (((φψ) ↔ χ) ↔ (φ ↔ (ψχ)))))
186, 17jaoi 635 . . 3 ((φ ¬ φ) → ((DECID ψ DECID χ) → (((φψ) ↔ χ) ↔ (φ ↔ (ψχ)))))
191, 18sylbi 114 . 2 (DECID φ → ((DECID ψ DECID χ) → (((φψ) ↔ χ) ↔ (φ ↔ (ψχ)))))
2019expd 245 1 (DECID φ → (DECID ψ → (DECID χ → (((φψ) ↔ χ) ↔ (φ ↔ (ψχ))))))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628  DECID wdc 741 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629 This theorem depends on definitions:  df-bi 110  df-dc 742 This theorem is referenced by:  bilukdc  1284
 Copyright terms: Public domain W3C validator