Lemma for nic-id. (Contributed by Jeff Hoffman, 17-Nov-2007.)
(Proof modification is discouraged.) (New usage is discouraged.)
\( \vdash (\theta \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge (((\varphi \barwedge (\chi \barwedge \psi)) \barwedge \theta) \barwedge ((\varphi \barwedge (\chi \barwedge \psi)) \barwedge \theta)) \)
\( \vdash (\varphi \barwedge (\chi \barwedge \psi)) \barwedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\varphi \barwedge \chi) \barwedge ((\varphi \barwedge \varphi) \barwedge (\varphi \barwedge \varphi)))) \)