Theorem nanass
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.)
Conclusion
\( \vdash \varphi \leftrightarrow \chi \leftrightarrow ((\varphi \barwedge \psi) \barwedge \chi \leftrightarrow \varphi \barwedge (\psi \barwedge \chi)) \)
Proof
l0
bicom1
nanbi2
l2
nanbi12d l0 _
l3
nannan
\( \vdash \varphi \barwedge (\psi \barwedge \chi) \leftrightarrow \varphi \rightarrow \psi \wedge \chi \)
simpr
imim2i _
\( \vdash (\varphi \rightarrow \psi \wedge \chi) \rightarrow \varphi \rightarrow \chi \)
l6
sylbi l3 _
l7
nannan
\( \vdash \chi \barwedge (\psi \barwedge \varphi) \leftrightarrow \chi \rightarrow \psi \wedge \varphi \)
simpr
imim2i _
\( \vdash (\chi \rightarrow \psi \wedge \varphi) \rightarrow \chi \rightarrow \varphi \)
sylbi l7 _
l11
impbid21d l6 _
l12
nanan
\( \vdash \varphi \wedge (\psi \barwedge \chi) \leftrightarrow \neg (\varphi \barwedge (\psi \barwedge \chi)) \)
simpl
\( \vdash \varphi \wedge (\psi \barwedge \chi) \rightarrow \varphi \)
l14
sylbir l12 _
\( \vdash \neg (\varphi \barwedge (\psi \barwedge \chi)) \rightarrow \varphi \)
l15
nanan
\( \vdash \chi \wedge (\psi \barwedge \varphi) \leftrightarrow \neg (\chi \barwedge (\psi \barwedge \varphi)) \)
simpl
\( \vdash \chi \wedge (\psi \barwedge \varphi) \rightarrow \chi \)
l17
sylbir l15 _
\( \vdash \neg (\chi \barwedge (\psi \barwedge \varphi)) \rightarrow \chi \)
pm5.1im
\( \vdash \varphi \rightarrow \chi \rightarrow (\varphi \leftrightarrow \chi) \)
syl2imc l14 l17 _
bija l11 _
l21
impbii l2 _
\( \vdash \varphi \leftrightarrow \chi \leftrightarrow (\chi \barwedge (\psi \barwedge \varphi) \leftrightarrow \varphi \barwedge (\psi \barwedge \chi)) \)
nancom
l23
nanbi2i _
\( \vdash \chi \barwedge (\psi \barwedge \varphi) \leftrightarrow \chi \barwedge (\varphi \barwedge \psi) \)
nancom
\( \vdash \chi \barwedge (\varphi \barwedge \psi) \leftrightarrow (\varphi \barwedge \psi) \barwedge \chi \)
bitri l23 _
bibi1i _
\( \vdash \chi \barwedge (\psi \barwedge \varphi) \leftrightarrow \varphi \barwedge (\psi \barwedge \chi) \leftrightarrow ((\varphi \barwedge \psi) \barwedge \chi \leftrightarrow \varphi \barwedge (\psi \barwedge \chi)) \)
bitri l21 _