Theorem biassdc 1385

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 825	. . 3 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2		pm5.501 243	. . . . . . 7 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ↔ 𝜓)))
3	2	bibi1d 232	. . . . . 6 ⊢ (𝜑 → ((𝜓 ↔ 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒)))
4		pm5.501 243	. . . . . 6 ⊢ (𝜑 → ((𝜓 ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))))
5	3, 4	bitr3d 189	. . . . 5 ⊢ (𝜑 → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))))
6	5	a1d 22	. . . 4 ⊢ (𝜑 → ((DECID 𝜓 ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒)))))
7		nbbndc 1384	. . . . . . . . 9 ⊢ (DECID 𝜓 → (DECID 𝜒 → ((¬ 𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒))))
8	7	imp 123	. . . . . . . 8 ⊢ ((DECID 𝜓 ∧ DECID 𝜒) → ((¬ 𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒)))
9	8	adantl 275	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → ((¬ 𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒)))
10		nbn2 687	. . . . . . . . 9 ⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓)))
11	10	bibi1d 232	. . . . . . . 8 ⊢ (¬ 𝜑 → ((¬ 𝜓 ↔ 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒)))
12	11	adantr 274	. . . . . . 7 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → ((¬ 𝜓 ↔ 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒)))
13	9, 12	bitr3d 189	. . . . . 6 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → (¬ (𝜓 ↔ 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒)))
14		nbn2 687	. . . . . . 7 ⊢ (¬ 𝜑 → (¬ (𝜓 ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))))
15	14	adantr 274	. . . . . 6 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → (¬ (𝜓 ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))))
16	13, 15	bitr3d 189	. . . . 5 ⊢ ((¬ 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))))
17	16	ex 114	. . . 4 ⊢ (¬ 𝜑 → ((DECID 𝜓 ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒)))))
18	6, 17	jaoi 706	. . 3 ⊢ ((𝜑 ∨ ¬ 𝜑) → ((DECID 𝜓 ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒)))))
19	1, 18	sylbi 120	. 2 ⊢ (DECID 𝜑 → ((DECID 𝜓 ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒)))))
20	19	expd 256	1 ⊢ (DECID 𝜑 → (DECID 𝜓 → (DECID 𝜒 → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 824

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 604  ax-in2 605  ax-io 699

This theorem depends on definitions:  df-bi 116  df-stab 821  df-dc 825

This theorem is referenced by:  bilukdc  1386