Theorem nanass 1499

Description: A characterization of when an expression involving alternative denials associates. Remark: alternative denial is commutative, see nancom 1485. (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 223	. . . 4 ⊢ ((𝜑 ↔ 𝜒) → (𝜒 ↔ 𝜑))
2		nanbi2 1491	. . . 4 ⊢ ((𝜑 ↔ 𝜒) → ((𝜓 ⊼ 𝜑) ↔ (𝜓 ⊼ 𝜒)))
3	1, 2	nanbi12d 1498	. . 3 ⊢ ((𝜑 ↔ 𝜒) → ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
4		nannan 1486	. . . . . 6 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒)))
5		simpr 487	. . . . . . 7 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
6	5	imim2i 16	. . . . . 6 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜒))
7	4, 6	sylbi 219	. . . . 5 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 → 𝜒))
8		nannan 1486	. . . . . 6 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜒 → (𝜓 ∧ 𝜑)))
9		simpr 487	. . . . . . 7 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
10	9	imim2i 16	. . . . . 6 ⊢ ((𝜒 → (𝜓 ∧ 𝜑)) → (𝜒 → 𝜑))
11	8, 10	sylbi 219	. . . . 5 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) → (𝜒 → 𝜑))
12	7, 11	impbid21d 213	. . . 4 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) → ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 ↔ 𝜒)))
13		nanan 1482	. . . . . 6 ⊢ ((𝜑 ∧ (𝜓 ⊼ 𝜒)) ↔ ¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)))
14		simpl 485	. . . . . 6 ⊢ ((𝜑 ∧ (𝜓 ⊼ 𝜒)) → 𝜑)
15	13, 14	sylbir 237	. . . . 5 ⊢ (¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)) → 𝜑)
16		nanan 1482	. . . . . 6 ⊢ ((𝜒 ∧ (𝜓 ⊼ 𝜑)) ↔ ¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)))
17		simpl 485	. . . . . 6 ⊢ ((𝜒 ∧ (𝜓 ⊼ 𝜑)) → 𝜒)
18	16, 17	sylbir 237	. . . . 5 ⊢ (¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)) → 𝜒)
19		pm5.1im 265	. . . . 5 ⊢ (𝜑 → (𝜒 → (𝜑 ↔ 𝜒)))
20	15, 18, 19	syl2imc 41	. . . 4 ⊢ (¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑)) → (¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 ↔ 𝜒)))
21	12, 20	bija 384	. . 3 ⊢ (((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) → (𝜑 ↔ 𝜒))
22	3, 21	impbii 211	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
23		nancom 1485	. . . . 5 ⊢ ((𝜓 ⊼ 𝜑) ↔ (𝜑 ⊼ 𝜓))
24	23	nanbi2i 1494	. . . 4 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜒 ⊼ (𝜑 ⊼ 𝜓)))
25		nancom 1485	. . . 4 ⊢ ((𝜒 ⊼ (𝜑 ⊼ 𝜓)) ↔ ((𝜑 ⊼ 𝜓) ⊼ 𝜒))
26	24, 25	bitri 277	. . 3 ⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ ((𝜑 ⊼ 𝜓) ⊼ 𝜒))
27	26	bibi1i 341	. 2 ⊢ (((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))
28	22, 27	bitri 277	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ⊼ wnan 1480

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

This theorem is referenced by: (None)