Theorem norass 1537

Description: A characterization of when an expression involving joint denials associates. This is identical to the case when alternative denial is associative, see nanass 1510. Remark: Like alternative denial, joint denial is also commutative, see norcom 1530. (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 319	. 2 ⊢ ((((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ⊽ 𝜒))) ↔ (¬ ((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ ¬ (𝜑 ∨ (𝜓 ⊽ 𝜒))))
2		norasslem1 1534	. . . 4 ⊢ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ⊽ 𝜑) ∨ 𝜒))
3		norasslem1 1534	. . . 4 ⊢ (((𝜓 ∨ 𝜒) → 𝜑) ↔ ((𝜓 ⊽ 𝜒) ∨ 𝜑))
4	2, 3	bibi12i 339	. . 3 ⊢ ((((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑)) ↔ (((𝜓 ⊽ 𝜑) ∨ 𝜒) ↔ ((𝜓 ⊽ 𝜒) ∨ 𝜑)))
5		bicom 222	. . . . 5 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜒 ↔ 𝜑))
6		norasslem2 1535	. . . . . 6 ⊢ (𝜓 → (𝜒 ↔ ((𝜓 ∨ 𝜑) → 𝜒)))
7		norasslem2 1535	. . . . . 6 ⊢ (𝜓 → (𝜑 ↔ ((𝜓 ∨ 𝜒) → 𝜑)))
8	6, 7	bibi12d 345	. . . . 5 ⊢ (𝜓 → ((𝜒 ↔ 𝜑) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑))))
9	5, 8	bitrid 283	. . . 4 ⊢ (𝜓 → ((𝜑 ↔ 𝜒) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑))))
10		impimprbi 829	. . . . 5 ⊢ ((𝜑 ↔ 𝜒) ↔ ((𝜑 → 𝜒) ↔ (𝜒 → 𝜑)))
11		norasslem3 1536	. . . . . 6 ⊢ (¬ 𝜓 → ((𝜑 → 𝜒) ↔ ((𝜓 ∨ 𝜑) → 𝜒)))
12		norasslem3 1536	. . . . . 6 ⊢ (¬ 𝜓 → ((𝜒 → 𝜑) ↔ ((𝜓 ∨ 𝜒) → 𝜑)))
13	11, 12	bibi12d 345	. . . . 5 ⊢ (¬ 𝜓 → (((𝜑 → 𝜒) ↔ (𝜒 → 𝜑)) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑))))
14	10, 13	bitrid 283	. . . 4 ⊢ (¬ 𝜓 → ((𝜑 ↔ 𝜒) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑))))
15	9, 14	pm2.61i 182	. . 3 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑)))
16		norcom 1530	. . . . 5 ⊢ ((𝜑 ⊽ 𝜓) ↔ (𝜓 ⊽ 𝜑))
17	16	orbi1i 914	. . . 4 ⊢ (((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ ((𝜓 ⊽ 𝜑) ∨ 𝜒))
18		orcom 871	. . . 4 ⊢ ((𝜑 ∨ (𝜓 ⊽ 𝜒)) ↔ ((𝜓 ⊽ 𝜒) ∨ 𝜑))
19	17, 18	bibi12i 339	. . 3 ⊢ ((((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ⊽ 𝜒))) ↔ (((𝜓 ⊽ 𝜑) ∨ 𝜒) ↔ ((𝜓 ⊽ 𝜒) ∨ 𝜑)))
20	4, 15, 19	3bitr4i 303	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ⊽ 𝜒))))
21		df-nor 1529	. . 3 ⊢ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ ¬ ((𝜑 ⊽ 𝜓) ∨ 𝜒))
22		df-nor 1529	. . 3 ⊢ ((𝜑 ⊽ (𝜓 ⊽ 𝜒)) ↔ ¬ (𝜑 ∨ (𝜓 ⊽ 𝜒)))
23	21, 22	bibi12i 339	. 2 ⊢ ((((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))) ↔ (¬ ((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ ¬ (𝜑 ∨ (𝜓 ⊽ 𝜒))))
24	1, 20, 23	3bitr4i 303	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 848   ⊽ wnor 1528

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 207  df-an 396  df-or 849  df-nor 1529

This theorem is referenced by: (None)