Theorem nic-id

Theorem id expressed with -/\. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \tau \barwedge (\tau \barwedge \tau) \)
Proof
nic-ax
\( \vdash (\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\tau \barwedge \tau) \barwedge ((\tau \barwedge \tau) \barwedge (\tau \barwedge \tau)))) \)
l1
nic-idlem2 _
\( \vdash (((\tau \barwedge \tau) \barwedge ((\tau \barwedge \tau) \barwedge (\tau \barwedge \tau))) \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge (\tau \barwedge (\tau \barwedge \tau)) \)
nic-idlem1
\( \vdash ((\tau \barwedge (\tau \barwedge \tau)) \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge ((((\tau \barwedge \tau) \barwedge ((\tau \barwedge \tau) \barwedge (\tau \barwedge \tau))) \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge (((\tau \barwedge \tau) \barwedge ((\tau \barwedge \tau) \barwedge (\tau \barwedge \tau))) \barwedge (\tau \barwedge (\tau \barwedge \tau)))) \)
nic-idlem2 _
\( \vdash ((((\tau \barwedge \tau) \barwedge ((\tau \barwedge \tau) \barwedge (\tau \barwedge \tau))) \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge (\tau \barwedge (\tau \barwedge \tau))) \)
nic-mp l1 _