Theorem nic-idlem2

Lemma for nic-id. Inference used by nic-id. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis
nic-idlem2.1
\( \vdash \eta \barwedge ((\varphi \barwedge (\chi \barwedge \psi)) \barwedge \theta) \)
Conclusion
\( \vdash (\theta \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge \eta \)
Proof
l0
nic-idlem2.1
\( \vdash \eta \barwedge ((\varphi \barwedge (\chi \barwedge \psi)) \barwedge \theta) \)
nic-ax
\( \vdash (\varphi \barwedge (\chi \barwedge \psi)) \barwedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\varphi \barwedge \chi) \barwedge ((\varphi \barwedge \varphi) \barwedge (\varphi \barwedge \varphi)))) \)
nic-imp _
\( \vdash (\theta \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge (((\varphi \barwedge (\chi \barwedge \psi)) \barwedge \theta) \barwedge ((\varphi \barwedge (\chi \barwedge \psi)) \barwedge \theta)) \)
nic-imp _
\( \vdash (\eta \barwedge ((\varphi \barwedge (\chi \barwedge \psi)) \barwedge \theta)) \barwedge (((\theta \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge \eta) \barwedge ((\theta \barwedge (\tau \barwedge (\tau \barwedge \tau))) \barwedge \eta)) \)
nic-mp l0 _