Theorem renicax
A rederivation of nic-ax from lukshef-ax1, proving that lukshef-ax1
with nic-mp can be used as a complete axiomatization of propositional
calculus. (Contributed by Anthony Hart, 31-Jul-2011.)
(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
l0
lukshefth1
\( \vdash (((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge (\varphi \barwedge (\chi \barwedge \psi)) \)
lukshefth2
\( \vdash ((((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge (\varphi \barwedge (\chi \barwedge \psi))) \barwedge (((\varphi \barwedge (\chi \barwedge \psi)) \barwedge (((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \barwedge (\tau \barwedge (\tau \barwedge \tau)))) \barwedge ((\varphi \barwedge (\chi \barwedge \psi)) \barwedge (((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \barwedge (\tau \barwedge (\tau \barwedge \tau))))) \)
l2
nic-mp l0 _
\( \vdash (\varphi \barwedge (\chi \barwedge \psi)) \barwedge (((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \barwedge (\tau \barwedge (\tau \barwedge \tau))) \)
l3
lukshefth2
\( \vdash ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \barwedge ((((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge (((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \barwedge (\tau \barwedge (\tau \barwedge \tau)))) \)
lukshef-ax1
\( \vdash (((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \barwedge ((((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge (((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \barwedge (\tau \barwedge (\tau \barwedge \tau))))) \barwedge (((\varphi \barwedge (\chi \barwedge \psi)) \barwedge ((\varphi \barwedge (\chi \barwedge \psi)) \barwedge (\varphi \barwedge (\chi \barwedge \psi)))) \barwedge (((\varphi \barwedge (\chi \barwedge \psi)) \barwedge (((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \barwedge (\tau \barwedge (\tau \barwedge \tau)))) \barwedge ((((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \barwedge (\varphi \barwedge (\chi \barwedge \psi))) \barwedge (((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \barwedge (\varphi \barwedge (\chi \barwedge \psi)))))) \)
nic-mp l3 _
\( \vdash ((\varphi \barwedge (\chi \barwedge \psi)) \barwedge (((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \barwedge (\tau \barwedge (\tau \barwedge \tau)))) \barwedge ((((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \barwedge (\varphi \barwedge (\chi \barwedge \psi))) \barwedge (((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \barwedge (\varphi \barwedge (\chi \barwedge \psi)))) \)
l6
nic-mp l2 _
\( \vdash ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \barwedge (\varphi \barwedge (\chi \barwedge \psi)) \)
lukshefth2
\( \vdash (((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \barwedge (\varphi \barwedge (\chi \barwedge \psi))) \barwedge (((\varphi \barwedge (\chi \barwedge \psi)) \barwedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))))) \barwedge ((\varphi \barwedge (\chi \barwedge \psi)) \barwedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))))) \)
nic-mp l6 _