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 ⊢φ↔χ↔φ⊽ψ⊽χ↔φ⊽ψ⊽χ