Metamath Proof Explorer

Theorem norass

Description: A characterization of when an expression involving joint denials associates. This is identical to the case when alternative denial is associative, see nanass . Remark: Like alternative denial, joint denial is also commutative, see norcom . (Contributed by RP, 29-Oct-2023) (Proof shortened by Wolf Lammen, 17-Dec-2023)

Ref Expression
Assertion norass ⊢ φ ↔ χ ↔ φ ⊽ ψ ⊽ χ ↔ φ ⊽ ψ ⊽ χ

Proof

Step Hyp Ref Expression
1 notbi ⊢ φ ⊽ ψ ∨ χ ↔ φ ∨ ψ ⊽ χ ↔ ¬ φ ⊽ ψ ∨ χ ↔ ¬ φ ∨ ψ ⊽ χ
2 norasslem1 ⊢ ψ ∨ φ → χ ↔ ψ ⊽ φ ∨ χ
3 norasslem1 ⊢ ψ ∨ χ → φ ↔ ψ ⊽ χ ∨ φ
4 2 3 bibi12i ⊢ ψ ∨ φ → χ ↔ ψ ∨ χ → φ ↔ ψ ⊽ φ ∨ χ ↔ ψ ⊽ χ ∨ φ
5 bicom ⊢ φ ↔ χ ↔ χ ↔ φ
6 norasslem2 ⊢ ψ → χ ↔ ψ ∨ φ → χ
7 norasslem2 ⊢ ψ → φ ↔ ψ ∨ χ → φ
8 6 7 bibi12d ⊢ ψ → χ ↔ φ ↔ ψ ∨ φ → χ ↔ ψ ∨ χ → φ
9 5 8 bitrid ⊢ ψ → φ ↔ χ ↔ ψ ∨ φ → χ ↔ ψ ∨ χ → φ
10 impimprbi ⊢ φ ↔ χ ↔ φ → χ ↔ χ → φ
11 norasslem3 ⊢ ¬ ψ → φ → χ ↔ ψ ∨ φ → χ
12 norasslem3 ⊢ ¬ ψ → χ → φ ↔ ψ ∨ χ → φ
13 11 12 bibi12d ⊢ ¬ ψ → φ → χ ↔ χ → φ ↔ ψ ∨ φ → χ ↔ ψ ∨ χ → φ
14 10 13 bitrid ⊢ ¬ ψ → φ ↔ χ ↔ ψ ∨ φ → χ ↔ ψ ∨ χ → φ
15 9 14 pm2.61i ⊢ φ ↔ χ ↔ ψ ∨ φ → χ ↔ ψ ∨ χ → φ
16 norcom ⊢ φ ⊽ ψ ↔ ψ ⊽ φ
17 16 orbi1i ⊢ φ ⊽ ψ ∨ χ ↔ ψ ⊽ φ ∨ χ
18 orcom ⊢ φ ∨ ψ ⊽ χ ↔ ψ ⊽ χ ∨ φ
19 17 18 bibi12i ⊢ φ ⊽ ψ ∨ χ ↔ φ ∨ ψ ⊽ χ ↔ ψ ⊽ φ ∨ χ ↔ ψ ⊽ χ ∨ φ
20 4 15 19 3bitr4i ⊢ φ ↔ χ ↔ φ ⊽ ψ ∨ χ ↔ φ ∨ ψ ⊽ χ
21 df-nor ⊢ φ ⊽ ψ ⊽ χ ↔ ¬ φ ⊽ ψ ∨ χ
22 df-nor ⊢ φ ⊽ ψ ⊽ χ ↔ ¬ φ ∨ ψ ⊽ χ
23 21 22 bibi12i ⊢ φ ⊽ ψ ⊽ χ ↔ φ ⊽ ψ ⊽ χ ↔ ¬ φ ⊽ ψ ∨ χ ↔ ¬ φ ∨ ψ ⊽ χ
24 1 20 23 3bitr4i ⊢ φ ↔ χ ↔ φ ⊽ ψ ⊽ χ ↔ φ ⊽ ψ ⊽ χ