Theorem norass 1567

Description: A characterization of when an expression involving joint denials associates. This is identical to the case when alternative denial is associative, see nanass 1540. Remark: Like alternative denial, joint denial is also commutative, see norcom 1560. (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 322	. 2 ⊢ ((((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ⊽ 𝜒))) ↔ (¬ ((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ ¬ (𝜑 ∨ (𝜓 ⊽ 𝜒))))
2		norasslem1 1564	. . . 4 ⊢ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ⊽ 𝜑) ∨ 𝜒))
3		norasslem1 1564	. . . 4 ⊢ (((𝜓 ∨ 𝜒) → 𝜑) ↔ ((𝜓 ⊽ 𝜒) ∨ 𝜑))
4	2, 3	bibi12i 342	. . 3 ⊢ ((((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑)) ↔ (((𝜓 ⊽ 𝜑) ∨ 𝜒) ↔ ((𝜓 ⊽ 𝜒) ∨ 𝜑)))
5		bicom 225	. . . . 5 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜒 ↔ 𝜑))
6		norasslem2 1565	. . . . . 6 ⊢ (𝜓 → (𝜒 ↔ ((𝜓 ∨ 𝜑) → 𝜒)))
7		norasslem2 1565	. . . . . 6 ⊢ (𝜓 → (𝜑 ↔ ((𝜓 ∨ 𝜒) → 𝜑)))
8	6, 7	bibi12d 348	. . . . 5 ⊢ (𝜓 → ((𝜒 ↔ 𝜑) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑))))
9	5, 8	bitrid 286	. . . 4 ⊢ (𝜓 → ((𝜑 ↔ 𝜒) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑))))
10		impimprbi 842	. . . . 5 ⊢ ((𝜑 ↔ 𝜒) ↔ ((𝜑 → 𝜒) ↔ (𝜒 → 𝜑)))
11		norasslem3 1566	. . . . . 6 ⊢ (¬ 𝜓 → ((𝜑 → 𝜒) ↔ ((𝜓 ∨ 𝜑) → 𝜒)))
12		norasslem3 1566	. . . . . 6 ⊢ (¬ 𝜓 → ((𝜒 → 𝜑) ↔ ((𝜓 ∨ 𝜒) → 𝜑)))
13	11, 12	bibi12d 348	. . . . 5 ⊢ (¬ 𝜓 → (((𝜑 → 𝜒) ↔ (𝜒 → 𝜑)) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑))))
14	10, 13	bitrid 286	. . . 4 ⊢ (¬ 𝜓 → ((𝜑 ↔ 𝜒) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑))))
15	9, 14	pm2.61i 184	. . 3 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜓 ∨ 𝜑) → 𝜒) ↔ ((𝜓 ∨ 𝜒) → 𝜑)))
16		norcom 1560	. . . . 5 ⊢ ((𝜑 ⊽ 𝜓) ↔ (𝜓 ⊽ 𝜑))
17	16	orbi1i 927	. . . 4 ⊢ (((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ ((𝜓 ⊽ 𝜑) ∨ 𝜒))
18		orcom 884	. . . 4 ⊢ ((𝜑 ∨ (𝜓 ⊽ 𝜒)) ↔ ((𝜓 ⊽ 𝜒) ∨ 𝜑))
19	17, 18	bibi12i 342	. . 3 ⊢ ((((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ⊽ 𝜒))) ↔ (((𝜓 ⊽ 𝜑) ∨ 𝜒) ↔ ((𝜓 ⊽ 𝜒) ∨ 𝜑)))
20	4, 15, 19	3bitr4i 306	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ⊽ 𝜒))))
21		df-nor 1559	. . 3 ⊢ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ ¬ ((𝜑 ⊽ 𝜓) ∨ 𝜒))
22		df-nor 1559	. . 3 ⊢ ((𝜑 ⊽ (𝜓 ⊽ 𝜒)) ↔ ¬ (𝜑 ∨ (𝜓 ⊽ 𝜒)))
23	21, 22	bibi12i 342	. 2 ⊢ ((((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))) ↔ (¬ ((𝜑 ⊽ 𝜓) ∨ 𝜒) ↔ ¬ (𝜑 ∨ (𝜓 ⊽ 𝜒))))
24	1, 20, 23	3bitr4i 306	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊽ 𝜓) ⊽ 𝜒) ↔ (𝜑 ⊽ (𝜓 ⊽ 𝜒))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861   ⊽ wnor 1558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-nor 1559

This theorem is used by: (None)