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

Theorem biassdc 1373
 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 820 . . 3 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2 pm5.501 243 . . . . . . 7 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
32bibi1d 232 . . . . . 6 (𝜑 → ((𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
4 pm5.501 243 . . . . . 6 (𝜑 → ((𝜓𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
53, 4bitr3d 189 . . . . 5 (𝜑 → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
65a1d 22 . . . 4 (𝜑 → ((DECID 𝜓DECID 𝜒) → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒)))))
7 nbbndc 1372 . . . . . . . . 9 (DECID 𝜓 → (DECID 𝜒 → ((¬ 𝜓𝜒) ↔ ¬ (𝜓𝜒))))
87imp 123 . . . . . . . 8 ((DECID 𝜓DECID 𝜒) → ((¬ 𝜓𝜒) ↔ ¬ (𝜓𝜒)))
98adantl 275 . . . . . . 7 ((¬ 𝜑 ∧ (DECID 𝜓DECID 𝜒)) → ((¬ 𝜓𝜒) ↔ ¬ (𝜓𝜒)))
10 nbn2 686 . . . . . . . . 9 𝜑 → (¬ 𝜓 ↔ (𝜑𝜓)))
1110bibi1d 232 . . . . . . . 8 𝜑 → ((¬ 𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
1211adantr 274 . . . . . . 7 ((¬ 𝜑 ∧ (DECID 𝜓DECID 𝜒)) → ((¬ 𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
139, 12bitr3d 189 . . . . . 6 ((¬ 𝜑 ∧ (DECID 𝜓DECID 𝜒)) → (¬ (𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
14 nbn2 686 . . . . . . 7 𝜑 → (¬ (𝜓𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
1514adantr 274 . . . . . 6 ((¬ 𝜑 ∧ (DECID 𝜓DECID 𝜒)) → (¬ (𝜓𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
1613, 15bitr3d 189 . . . . 5 ((¬ 𝜑 ∧ (DECID 𝜓DECID 𝜒)) → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
1716ex 114 . . . 4 𝜑 → ((DECID 𝜓DECID 𝜒) → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒)))))
186, 17jaoi 705 . . 3 ((𝜑 ∨ ¬ 𝜑) → ((DECID 𝜓DECID 𝜒) → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒)))))
191, 18sylbi 120 . 2 (DECID 𝜑 → ((DECID 𝜓DECID 𝜒) → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒)))))
2019expd 256 1 (DECID 𝜑 → (DECID 𝜓 → (DECID 𝜒 → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697  DECID wdc 819 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 603  ax-in2 604  ax-io 698 This theorem depends on definitions:  df-bi 116  df-stab 816  df-dc 820 This theorem is referenced by:  bilukdc  1374
 Copyright terms: Public domain W3C validator