Theorem norass 1533

Description: A characterization of when an expression involving joint denials associates. This is identical to the case when alternative denial is associative, see nanass 1500. Remark: Like alternative denial, joint denial is also commutative, see norcom 1522. (Contributed by RP, 29-Oct-2023.) (Proof shortened by Wolf Lammen, 17-Dec-2023.)

Assertion

Ref	Expression
norass	⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))))

Proof of Theorem norass

Step	Hyp	Ref	Expression
1		notbi 321	. 2 ⊢ ((((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ⊽ 𝜒))) ↔ (¬ ((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ ¬ (𝜑 ∨ (𝜓 ⊽ 𝜒))))
2		norasslem1 1530	. . . 4 ⊢ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ⊽ 𝜑) ∨ 𝜒))
3		norasslem1 1530	. . . 4 ⊢ (((𝜓 ∨ 𝜒) → 𝜑) ↔ ((𝜓 ⊽ 𝜒) ∨ 𝜑))
4	2, 3	bibi12i 342	. . 3 ⊢ ((((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑)) ↔ (((𝜓 ⊽ 𝜑) ∨ 𝜒) ↔ ((𝜓 ⊽ 𝜒) ∨ 𝜑)))
5		bicom 224	. . . . 5 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜒 ↔ 𝜑))
6		norasslem2 1531	. . . . . 6 ⊢ (𝜓 → (𝜒 ↔ ((𝜓 ∨ 𝜑) → 𝜒)))
7		norasslem2 1531	. . . . . 6 ⊢ (𝜓 → (𝜑 ↔ ((𝜓 ∨ 𝜒) → 𝜑)))
8	6, 7	bibi12d 348	. . . . 5 ⊢ (𝜓 → ((𝜒 ↔ 𝜑) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑))))
9	5, 8	syl5bb 285	. . . 4 ⊢ (𝜓 → ((𝜑 ↔ 𝜒) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑))))
10		impimprbi 826	. . . . 5 ⊢ ((𝜑 ↔ 𝜒) ↔ ((𝜑 → 𝜒) ↔ (𝜒 → 𝜑)))
11		norasslem3 1532	. . . . . 6 ⊢ (¬ 𝜓 → ((𝜑 → 𝜒) ↔ ((𝜓 ∨ 𝜑) → 𝜒)))
12		norasslem3 1532	. . . . . 6 ⊢ (¬ 𝜓 → ((𝜒 → 𝜑) ↔ ((𝜓 ∨ 𝜒) → 𝜑)))
13	11, 12	bibi12d 348	. . . . 5 ⊢ (¬ 𝜓 → (((𝜑 → 𝜒) ↔ (𝜒 → 𝜑)) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑))))
14	10, 13	syl5bb 285	. . . 4 ⊢ (¬ 𝜓 → ((𝜑 ↔ 𝜒) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑))))
15	9, 14	pm2.61i 184	. . 3 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑)))
16		norcom 1522	. . . . 5 ⊢ ((𝜑 ⊽ 𝜓) ↔ (𝜓 ⊽ 𝜑))
17	16	orbi1i 910	. . . 4 ⊢ (((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ ((𝜓 ⊽ 𝜑) ∨ 𝜒))
18		orcom 866	. . . 4 ⊢ ((𝜑 ∨ (𝜓 ⊽ 𝜒)) ↔ ((𝜓 ⊽ 𝜒) ∨ 𝜑))
19	17, 18	bibi12i 342	. . 3 ⊢ ((((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ⊽ 𝜒))) ↔ (((𝜓 ⊽ 𝜑) ∨ 𝜒) ↔ ((𝜓 ⊽ 𝜒) ∨ 𝜑)))
20	4, 15, 19	3bitr4i 305	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ⊽ 𝜒))))
21		df-nor 1521	. . 3 ⊢ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ ¬ ((𝜑 ⊽ 𝜓) ∨ 𝜒))
22		df-nor 1521	. . 3 ⊢ ((𝜑 ⊽ (𝜓 ⊽ 𝜒)) ↔ ¬ (𝜑 ∨ (𝜓 ⊽ 𝜒)))
23	21, 22	bibi12i 342	. 2 ⊢ ((((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))) ↔ (¬ ((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ ¬ (𝜑 ∨ (𝜓 ⊽ 𝜒))))
24	1, 20, 23	3bitr4i 305	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∨ wo 843   ⊽ wnor 1520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-nor 1521

This theorem is referenced by: (None)