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

Theorem biassdc 1327
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 777 . . 3 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2 pm5.501 242 . . . . . . 7 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
32bibi1d 231 . . . . . 6 (𝜑 → ((𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
4 pm5.501 242 . . . . . 6 (𝜑 → ((𝜓𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
53, 4bitr3d 188 . . . . 5 (𝜑 → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
65a1d 22 . . . 4 (𝜑 → ((DECID 𝜓DECID 𝜒) → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒)))))
7 nbbndc 1326 . . . . . . . . 9 (DECID 𝜓 → (DECID 𝜒 → ((¬ 𝜓𝜒) ↔ ¬ (𝜓𝜒))))
87imp 122 . . . . . . . 8 ((DECID 𝜓DECID 𝜒) → ((¬ 𝜓𝜒) ↔ ¬ (𝜓𝜒)))
98adantl 271 . . . . . . 7 ((¬ 𝜑 ∧ (DECID 𝜓DECID 𝜒)) → ((¬ 𝜓𝜒) ↔ ¬ (𝜓𝜒)))
10 nbn2 646 . . . . . . . . 9 𝜑 → (¬ 𝜓 ↔ (𝜑𝜓)))
1110bibi1d 231 . . . . . . . 8 𝜑 → ((¬ 𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
1211adantr 270 . . . . . . 7 ((¬ 𝜑 ∧ (DECID 𝜓DECID 𝜒)) → ((¬ 𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
139, 12bitr3d 188 . . . . . 6 ((¬ 𝜑 ∧ (DECID 𝜓DECID 𝜒)) → (¬ (𝜓𝜒) ↔ ((𝜑𝜓) ↔ 𝜒)))
14 nbn2 646 . . . . . . 7 𝜑 → (¬ (𝜓𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
1514adantr 270 . . . . . 6 ((¬ 𝜑 ∧ (DECID 𝜓DECID 𝜒)) → (¬ (𝜓𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
1613, 15bitr3d 188 . . . . 5 ((¬ 𝜑 ∧ (DECID 𝜓DECID 𝜒)) → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))
1716ex 113 . . . 4 𝜑 → ((DECID 𝜓DECID 𝜒) → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒)))))
186, 17jaoi 669 . . 3 ((𝜑 ∨ ¬ 𝜑) → ((DECID 𝜓DECID 𝜒) → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒)))))
191, 18sylbi 119 . 2 (DECID 𝜑 → ((DECID 𝜓DECID 𝜒) → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒)))))
2019expd 254 1 (DECID 𝜑 → (DECID 𝜓 → (DECID 𝜒 → (((𝜑𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓𝜒))))))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 662  DECID wdc 776
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663
This theorem depends on definitions:  df-bi 115  df-dc 777
This theorem is referenced by:  bilukdc  1328
  Copyright terms: Public domain W3C validator