Theorem norass
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.)
Conclusion
\( \vdash \varphi \leftrightarrow \chi \leftrightarrow ((\varphi \mathbin{\overline{\vee}} \psi) \mathbin{\overline{\vee}} \chi \leftrightarrow \varphi \mathbin{\overline{\vee}} (\psi \mathbin{\overline{\vee}} \chi)) \)
Proof
l0
notbi
\( \vdash \varphi \mathbin{\overline{\vee}} \psi \vee \chi \leftrightarrow \varphi \vee (\psi \mathbin{\overline{\vee}} \chi) \leftrightarrow (\neg (\varphi \mathbin{\overline{\vee}} \psi \vee \chi) \leftrightarrow \neg (\varphi \vee (\psi \mathbin{\overline{\vee}} \chi))) \)
l1
norasslem1
norasslem1
l3
bibi12i l1 _
\( \vdash \psi \vee \varphi \rightarrow \chi \leftrightarrow \psi \vee \chi \rightarrow \varphi \leftrightarrow (\psi \mathbin{\overline{\vee}} \varphi \vee \chi \leftrightarrow \psi \mathbin{\overline{\vee}} \chi \vee \varphi) \)
l4
bicom
\( \vdash \varphi \leftrightarrow \chi \leftrightarrow (\chi \leftrightarrow \varphi) \)
l5
norasslem2
norasslem2
bibi12d l5 _
\( \vdash \psi \rightarrow (\chi \leftrightarrow \varphi \leftrightarrow (\psi \vee \varphi \rightarrow \chi \leftrightarrow \psi \vee \chi \rightarrow \varphi)) \)
l8
bitrid l4 _
\( \vdash \psi \rightarrow (\varphi \leftrightarrow \chi \leftrightarrow (\psi \vee \varphi \rightarrow \chi \leftrightarrow \psi \vee \chi \rightarrow \varphi)) \)
l9
impimprbi
\( \vdash \varphi \leftrightarrow \chi \leftrightarrow (\varphi \rightarrow \chi \leftrightarrow \chi \rightarrow \varphi) \)
l10
norasslem3
norasslem3
bibi12d l10 _
\( \vdash \neg \psi \rightarrow (\varphi \rightarrow \chi \leftrightarrow \chi \rightarrow \varphi \leftrightarrow (\psi \vee \varphi \rightarrow \chi \leftrightarrow \psi \vee \chi \rightarrow \varphi)) \)
bitrid l9 _
\( \vdash \neg \psi \rightarrow (\varphi \leftrightarrow \chi \leftrightarrow (\psi \vee \varphi \rightarrow \chi \leftrightarrow \psi \vee \chi \rightarrow \varphi)) \)
l14
pm2.61i l8 _
\( \vdash \varphi \leftrightarrow \chi \leftrightarrow (\psi \vee \varphi \rightarrow \chi \leftrightarrow \psi \vee \chi \rightarrow \varphi) \)
norcom
l16
orbi1i _
orcom
bibi12i l16 _
\( \vdash \varphi \mathbin{\overline{\vee}} \psi \vee \chi \leftrightarrow \varphi \vee (\psi \mathbin{\overline{\vee}} \chi) \leftrightarrow (\psi \mathbin{\overline{\vee}} \varphi \vee \chi \leftrightarrow \psi \mathbin{\overline{\vee}} \chi \vee \varphi) \)
l19
3bitr4i l3 l14 _
\( \vdash \varphi \leftrightarrow \chi \leftrightarrow (\varphi \mathbin{\overline{\vee}} \psi \vee \chi \leftrightarrow \varphi \vee (\psi \mathbin{\overline{\vee}} \chi)) \)
l20
df-nor
df-nor
bibi12i l20 _
\( \vdash (\varphi \mathbin{\overline{\vee}} \psi) \mathbin{\overline{\vee}} \chi \leftrightarrow \varphi \mathbin{\overline{\vee}} (\psi \mathbin{\overline{\vee}} \chi) \leftrightarrow (\neg (\varphi \mathbin{\overline{\vee}} \psi \vee \chi) \leftrightarrow \neg (\varphi \vee (\psi \mathbin{\overline{\vee}} \chi))) \)
3bitr4i l0 l19 _