Theorem nanass

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

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

Proof

Step	Hyp	Ref	Expression
1		bicom1	⊢ ( ( 𝜑 ↔ 𝜒 ) → ( 𝜒 ↔ 𝜑 ) )
2		nanbi2	⊢ ( ( 𝜑 ↔ 𝜒 ) → ( ( 𝜓 ⊼ 𝜑 ) ↔ ( 𝜓 ⊼ 𝜒 ) ) )
3	1 2	nanbi12d	⊢ ( ( 𝜑 ↔ 𝜒 ) → ( ( 𝜒 ⊼ ( 𝜓 ⊼ 𝜑 ) ) ↔ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ) )
4		nannan	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ↔ ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) )
5		simpr	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜒 )
6	5	imim2i	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( 𝜑 → 𝜒 ) )
7	4 6	sylbi	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) → ( 𝜑 → 𝜒 ) )
8		nannan	⊢ ( ( 𝜒 ⊼ ( 𝜓 ⊼ 𝜑 ) ) ↔ ( 𝜒 → ( 𝜓 ∧ 𝜑 ) ) )
9		simpr	⊢ ( ( 𝜓 ∧ 𝜑 ) → 𝜑 )
10	9	imim2i	⊢ ( ( 𝜒 → ( 𝜓 ∧ 𝜑 ) ) → ( 𝜒 → 𝜑 ) )
11	8 10	sylbi	⊢ ( ( 𝜒 ⊼ ( 𝜓 ⊼ 𝜑 ) ) → ( 𝜒 → 𝜑 ) )
12	7 11	impbid21d	⊢ ( ( 𝜒 ⊼ ( 𝜓 ⊼ 𝜑 ) ) → ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) → ( 𝜑 ↔ 𝜒 ) ) )
13		nanan	⊢ ( ( 𝜑 ∧ ( 𝜓 ⊼ 𝜒 ) ) ↔ ¬ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) )
14		simpl	⊢ ( ( 𝜑 ∧ ( 𝜓 ⊼ 𝜒 ) ) → 𝜑 )
15	13 14	sylbir	⊢ ( ¬ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) → 𝜑 )
16		nanan	⊢ ( ( 𝜒 ∧ ( 𝜓 ⊼ 𝜑 ) ) ↔ ¬ ( 𝜒 ⊼ ( 𝜓 ⊼ 𝜑 ) ) )
17		simpl	⊢ ( ( 𝜒 ∧ ( 𝜓 ⊼ 𝜑 ) ) → 𝜒 )
18	16 17	sylbir	⊢ ( ¬ ( 𝜒 ⊼ ( 𝜓 ⊼ 𝜑 ) ) → 𝜒 )
19		pm5.1im	⊢ ( 𝜑 → ( 𝜒 → ( 𝜑 ↔ 𝜒 ) ) )
20	15 18 19	syl2imc	⊢ ( ¬ ( 𝜒 ⊼ ( 𝜓 ⊼ 𝜑 ) ) → ( ¬ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) → ( 𝜑 ↔ 𝜒 ) ) )
21	12 20	bija	⊢ ( ( ( 𝜒 ⊼ ( 𝜓 ⊼ 𝜑 ) ) ↔ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ) → ( 𝜑 ↔ 𝜒 ) )
22	3 21	impbii	⊢ ( ( 𝜑 ↔ 𝜒 ) ↔ ( ( 𝜒 ⊼ ( 𝜓 ⊼ 𝜑 ) ) ↔ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ) )
23		nancom	⊢ ( ( 𝜓 ⊼ 𝜑 ) ↔ ( 𝜑 ⊼ 𝜓 ) )
24	23	nanbi2i	⊢ ( ( 𝜒 ⊼ ( 𝜓 ⊼ 𝜑 ) ) ↔ ( 𝜒 ⊼ ( 𝜑 ⊼ 𝜓 ) ) )
25		nancom	⊢ ( ( 𝜒 ⊼ ( 𝜑 ⊼ 𝜓 ) ) ↔ ( ( 𝜑 ⊼ 𝜓 ) ⊼ 𝜒 ) )
26	24 25	bitri	⊢ ( ( 𝜒 ⊼ ( 𝜓 ⊼ 𝜑 ) ) ↔ ( ( 𝜑 ⊼ 𝜓 ) ⊼ 𝜒 ) )
27	26	bibi1i	⊢ ( ( ( 𝜒 ⊼ ( 𝜓 ⊼ 𝜑 ) ) ↔ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ) ↔ ( ( ( 𝜑 ⊼ 𝜓 ) ⊼ 𝜒 ) ↔ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ) )
28	22 27	bitri	⊢ ( ( 𝜑 ↔ 𝜒 ) ↔ ( ( ( 𝜑 ⊼ 𝜓 ) ⊼ 𝜒 ) ↔ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ) )