Theorem lukshefth2
Lemma for renicax. (Contributed by NM, 31-Jul-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
Conclusion
\( \vdash (\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau)) \)
Proof
l0
lukshef-ax1
\( \vdash (\theta \barwedge (\theta \barwedge \theta)) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge ((\theta \barwedge \theta) \barwedge ((\theta \barwedge \theta) \barwedge (\theta \barwedge \theta)))) \)
lukshef-ax1
\( \vdash ((\theta \barwedge (\theta \barwedge \theta)) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge ((\theta \barwedge \theta) \barwedge ((\theta \barwedge \theta) \barwedge (\theta \barwedge \theta))))) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge ((\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta)))) \)
l2
nic-mp l0 _
\( \vdash (\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta)) \)
l3
lukshefth1
\( \vdash (((\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau))) \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (\theta \barwedge (\theta \barwedge \theta)) \)
l4
lukshef-ax1
\( \vdash ((\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta))) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge ((\theta \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta)) \barwedge (((\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge \theta) \barwedge ((\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge \theta)))) \)
lukshef-ax1
\( \vdash (((\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta))) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge ((\theta \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta)) \barwedge (((\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge \theta) \barwedge ((\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge \theta))))) \barwedge (((((\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau))) \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge ((((\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau))) \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (((\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau))) \barwedge (\theta \barwedge (\theta \barwedge \theta))))) \barwedge (((((\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau))) \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge ((((\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta))) \barwedge (((\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau))) \barwedge (\theta \barwedge (\theta \barwedge \theta)))) \barwedge (((\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta))) \barwedge (((\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau))) \barwedge (\theta \barwedge (\theta \barwedge \theta))))))) \)
nic-mp l4 _
\( \vdash ((((\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau))) \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge ((((\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta))) \barwedge (((\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau))) \barwedge (\theta \barwedge (\theta \barwedge \theta)))) \barwedge (((\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta))) \barwedge (((\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau))) \barwedge (\theta \barwedge (\theta \barwedge \theta))))) \)
nic-mp l3 _
\( \vdash ((\theta \barwedge (\theta \barwedge (\theta \barwedge \theta))) \barwedge (((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta) \barwedge ((\theta \barwedge (\theta \barwedge \theta)) \barwedge \theta))) \barwedge (((\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau))) \barwedge (\theta \barwedge (\theta \barwedge \theta))) \)
l8
nic-mp l2 _
\( \vdash \theta \barwedge (\theta \barwedge \theta) \)
lukshef-ax1
\( \vdash (\theta \barwedge (\theta \barwedge \theta)) \barwedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\tau \barwedge \theta) \barwedge ((\theta \barwedge \tau) \barwedge (\theta \barwedge \tau)))) \)
nic-mp l8 _