Theorem nanass 1539

Description: A characterization of when an expression involving alternative denials associates. Remark: alternative denial is commutative, see nancom 1525. (Contributed by Richard Penner, 29-Feb-2020.) (Proof shortened by Wolf Lammen, 23-Oct-2022.)

Assertion

Ref	Expression
nanass	⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))

Proof of Theorem nanass

Step	Hyp	Ref	Expression
1		bicom1 224	. . . 4 ⊢ ((𝜑 ↔ 𝜒) → (𝜒 ↔ 𝜑))
2		nanbi2 1531	. . . 4 ⊢ ((𝜑 ↔ 𝜒) → ((𝜓 ⊼ 𝜑) ↔ (𝜓 ⊼ 𝜒)))
3	1, 2	nanbi12d 1538	. . 3 ⊢ ((𝜑 ↔ 𝜒) → ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
4		nannan 1526	. . . . . 6 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒)))
5		simpr 490	. . . . . . 7 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
6	5	imim2i 17	. . . . . 6 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜒))
7	4, 6	sylbi 220	. . . . 5 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 → 𝜒))
8		nannan 1526	. . . . . 6 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜒 → (𝜓 ∧ 𝜑)))
9		simpr 490	. . . . . . 7 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
10	9	imim2i 17	. . . . . 6 ⊢ ((𝜒 → (𝜓 ∧ 𝜑)) → (𝜒 → 𝜑))
11	8, 10	sylbi 220	. . . . 5 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) → (𝜒 → 𝜑))
12	7, 11	impbid21d 214	. . . 4 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) → ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 ↔ 𝜒)))
13		nanan 1522	. . . . . 6 ⊢ ((𝜑 ∧ (𝜓 ⊼ 𝜒)) ↔ ¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)))
14		simpl 488	. . . . . 6 ⊢ ((𝜑 ∧ (𝜓 ⊼ 𝜒)) → 𝜑)
15	13, 14	sylbir 238	. . . . 5 ⊢ (¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)) → 𝜑)
16		nanan 1522	. . . . . 6 ⊢ ((𝜒 ∧ (𝜓 ⊼ 𝜑)) ↔ ¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)))
17		simpl 488	. . . . . 6 ⊢ ((𝜒 ∧ (𝜓 ⊼ 𝜑)) → 𝜒)
18	16, 17	sylbir 238	. . . . 5 ⊢ (¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)) → 𝜒)
19		pm5.1im 266	. . . . 5 ⊢ (𝜑 → (𝜒 → (𝜑 ↔ 𝜒)))
20	15, 18, 19	syl2imc 42	. . . 4 ⊢ (¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)) → (¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 ↔ 𝜒)))
21	12, 20	bija 383	. . 3 ⊢ (((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) → (𝜑 ↔ 𝜒))
22	3, 21	impbii 212	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
23		nancom 1525	. . . . 5 ⊢ ((𝜓 ⊼ 𝜑) ↔ (𝜑 ⊼ 𝜓))
24	23	nanbi2i 1534	. . . 4 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜒 ⊼ (𝜑 ⊼ 𝜓)))
25		nancom 1525	. . . 4 ⊢ ((𝜒 ⊼ (𝜑 ⊼ 𝜓)) ↔ ((𝜑 ⊼ 𝜓) ⊼ 𝜒))
26	24, 25	bitri 278	. . 3 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ ((𝜑 ⊼ 𝜓) ⊼ 𝜒))
27	26	bibi1i 341	. 2 ⊢ (((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
28	22, 27	bitri 278	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ⊼ wnan 1520

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-nan 1521

This theorem is used by: (None)