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