Theorem nic-axALT
A direct proof of nic-ax. (Contributed by NM, 11-Dec-2008.)
(Proof modification is discouraged.) (New usage is discouraged.)
Conclusion
\( \vdash (\varphi \barwedge (\chi \barwedge \psi)) \barwedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \)
Proof
simpl
l1
imim2i _
\( \vdash (\varphi \rightarrow \chi \wedge \psi) \rightarrow \varphi \rightarrow \chi \)
con3
imim2d _
\( \vdash (\varphi \rightarrow \chi) \rightarrow (\theta \rightarrow \neg \chi) \rightarrow \theta \rightarrow \neg \varphi \)
l4
syl l1 _
anidm
biimpri _
l7
jctil l4 _
\( \vdash (\varphi \rightarrow \chi \wedge \psi) \rightarrow (\tau \rightarrow \tau \wedge \tau) \wedge ((\theta \rightarrow \neg \chi) \rightarrow \theta \rightarrow \neg \varphi) \)
df-nan
anbi2i _
l10
notbii _
\( \vdash \neg (\varphi \wedge (\chi \barwedge \psi)) \leftrightarrow \neg (\varphi \wedge \neg (\chi \wedge \psi)) \)
l11
df-nan
\( \vdash \varphi \barwedge (\chi \barwedge \psi) \leftrightarrow \neg (\varphi \wedge (\chi \barwedge \psi)) \)
iman
\( \vdash \varphi \rightarrow \chi \wedge \psi \leftrightarrow \neg (\varphi \wedge \neg (\chi \wedge \psi)) \)
l13
3bitr4i l10 l11 _
l14
df-nan
\( \vdash (\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \leftrightarrow \neg ((\tau \barwedge (\tau \barwedge \tau)) \wedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \)
df-nan
anbi2i _
l17
notbii _
\( \vdash \neg (\tau \wedge (\tau \barwedge \tau)) \leftrightarrow \neg (\tau \wedge \neg (\tau \wedge \tau)) \)
l18
df-nan
\( \vdash \tau \barwedge (\tau \barwedge \tau) \leftrightarrow \neg (\tau \wedge (\tau \barwedge \tau)) \)
iman
\( \vdash \tau \rightarrow \tau \wedge \tau \leftrightarrow \neg (\tau \wedge \neg (\tau \wedge \tau)) \)
l20
3bitr4i l17 l18 _
l21
df-nan
\( \vdash \theta \barwedge \chi \leftrightarrow \neg (\theta \wedge \chi) \)
imnan
\( \vdash \theta \rightarrow \neg \chi \leftrightarrow \neg (\theta \wedge \chi) \)
l23
bitr4i l21 _
l24
df-nan
\( \vdash (\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta) \leftrightarrow \neg ((\varphi \barwedge \theta) \wedge (\varphi \barwedge \theta)) \)
l25
anidm
\( \vdash (\varphi \barwedge \theta) \wedge (\varphi \barwedge \theta) \leftrightarrow \varphi \barwedge \theta \)
l26
df-nan
\( \vdash \varphi \barwedge \theta \leftrightarrow \neg (\varphi \wedge \theta) \)
l27
imnan
\( \vdash \varphi \rightarrow \neg \theta \leftrightarrow \neg (\varphi \wedge \theta) \)
con2b
\( \vdash \varphi \rightarrow \neg \theta \leftrightarrow \theta \rightarrow \neg \varphi \)
bitr3i l27 _
\( \vdash \neg (\varphi \wedge \theta) \leftrightarrow \theta \rightarrow \neg \varphi \)
3bitri l25 l26 _
\( \vdash (\varphi \barwedge \theta) \wedge (\varphi \barwedge \theta) \leftrightarrow \theta \rightarrow \neg \varphi \)
xchbinx l24 _
anbi12i l23 _
l33
notbii _
\( \vdash \neg ((\theta \barwedge \chi) \wedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \leftrightarrow \neg ((\theta \rightarrow \neg \chi) \wedge \neg (\theta \rightarrow \neg \varphi)) \)
l34
df-nan
\( \vdash (\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)) \leftrightarrow \neg ((\theta \barwedge \chi) \wedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \)
iman
\( \vdash (\theta \rightarrow \neg \chi) \rightarrow \theta \rightarrow \neg \varphi \leftrightarrow \neg ((\theta \rightarrow \neg \chi) \wedge \neg (\theta \rightarrow \neg \varphi)) \)
3bitr4i l33 l34 _
anbi12i l20 _
\( \vdash (\tau \barwedge (\tau \barwedge \tau)) \wedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \leftrightarrow (\tau \rightarrow \tau \wedge \tau) \wedge ((\theta \rightarrow \neg \chi) \rightarrow \theta \rightarrow \neg \varphi) \)
xchbinx l14 _
anbi12i l13 _
l40
notbii _
\( \vdash \neg ((\varphi \barwedge (\chi \barwedge \psi)) \wedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))))) \leftrightarrow \neg ((\varphi \rightarrow \chi \wedge \psi) \wedge \neg ((\tau \rightarrow \tau \wedge \tau) \wedge ((\theta \rightarrow \neg \chi) \rightarrow \theta \rightarrow \neg \varphi))) \)
iman
\( \vdash (\varphi \rightarrow \chi \wedge \psi) \rightarrow (\tau \rightarrow \tau \wedge \tau) \wedge ((\theta \rightarrow \neg \chi) \rightarrow \theta \rightarrow \neg \varphi) \leftrightarrow \neg ((\varphi \rightarrow \chi \wedge \psi) \wedge \neg ((\tau \rightarrow \tau \wedge \tau) \wedge ((\theta \rightarrow \neg \chi) \rightarrow \theta \rightarrow \neg \varphi))) \)
bitr4i l40 _
\( \vdash \neg ((\varphi \barwedge (\chi \barwedge \psi)) \wedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))))) \leftrightarrow (\varphi \rightarrow \chi \wedge \psi) \rightarrow (\tau \rightarrow \tau \wedge \tau) \wedge ((\theta \rightarrow \neg \chi) \rightarrow \theta \rightarrow \neg \varphi) \)
l43
mpbir l7 _
\( \vdash \neg ((\varphi \barwedge (\chi \barwedge \psi)) \wedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))))) \)
df-nan
\( \vdash (\varphi \barwedge (\chi \barwedge \psi)) \barwedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \leftrightarrow \neg ((\varphi \barwedge (\chi \barwedge \psi)) \wedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))))) \)
mpbir l43 _