Theorem biassdc 1395

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 835	. . 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 1394	. . . . . . . . 9 ⊢ (DECID 𝜓 → (DECID 𝜒 → ((¬ 𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒))))
8	7	imp 124	. . . . . . . 8 ⊢ ((DECID 𝜓 ∧ DECID 𝜒) → ((¬ 𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒)))
9	8	adantl 277	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → ((¬ 𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒)))
10		nbn2 697	. . . . . . . . 9 ⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓)))
11	10	bibi1d 233	. . . . . . . 8 ⊢ (¬ 𝜑 → ((¬ 𝜓 ↔ 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒)))
12	11	adantr 276	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → ((¬ 𝜓 ↔ 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒)))
13	9, 12	bitr3d 190	. . . . . 6 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → (¬ (𝜓 ↔ 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒)))
14		nbn2 697	. . . . . . 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 716	. . 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 708  DECID wdc 834

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 614  ax-in2 615  ax-io 709

This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835

This theorem is referenced by:  bilukdc  1396