Theorem biassdc 1437

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

Step	Hyp	Ref	Expression
1		df-dc 840	. . 3 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2		pm5.501 244	. . . . . . 7 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ↔ 𝜓)))
3	2	bibi1d 233	. . . . . 6 ⊢ (𝜑 → ((𝜓 ↔ 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒)))
4		pm5.501 244	. . . . . 6 ⊢ (𝜑 → ((𝜓 ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))))
5	3, 4	bitr3d 190	. . . . 5 ⊢ (𝜑 → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))))
6	5	a1d 22	. . . 4 ⊢ (𝜑 → ((DECID 𝜓 ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒)))))
7		nbbndc 1436	. . . . . . . . 9 ⊢ (DECID 𝜓 → (DECID 𝜒 → ((¬ 𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒))))
8	7	imp 124	. . . . . . . 8 ⊢ ((DECID 𝜓 ∧ DECID 𝜒) → ((¬ 𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒)))
9	8	adantl 277	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → ((¬ 𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒)))
10		nbn2 702	. . . . . . . . 9 ⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓)))
11	10	bibi1d 233	. . . . . . . 8 ⊢ (¬ 𝜑 → ((¬ 𝜓 ↔ 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒)))
12	11	adantr 276	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → ((¬ 𝜓 ↔ 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒)))
13	9, 12	bitr3d 190	. . . . . 6 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → (¬ (𝜓 ↔ 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒)))
14		nbn2 702	. . . . . . 7 ⊢ (¬ 𝜑 → (¬ (𝜓 ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))))
15	14	adantr 276	. . . . . 6 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → (¬ (𝜓 ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))))
16	13, 15	bitr3d 190	. . . . 5 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))))
17	16	ex 115	. . . 4 ⊢ (¬ 𝜑 → ((DECID 𝜓 ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒)))))
18	6, 17	jaoi 721	. . 3 ⊢ ((𝜑 ∨ ¬ 𝜑) → ((DECID 𝜓 ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒)))))
19	1, 18	sylbi 121	. 2 ⊢ (DECID 𝜑 → ((DECID 𝜓 ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒)))))
20	19	expd 258	1 ⊢ (DECID 𝜑 → (DECID 𝜓 → (DECID 𝜒 → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 713  DECID wdc 839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714

This theorem depends on definitions:  df-bi 117  df-stab 836  df-dc 840

This theorem is referenced by:  bilukdc  1438