Theorem nic-ich

Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
nic-ich.1
\( \vdash \varphi \barwedge (\psi \barwedge \psi) \)
nic-ich.2
\( \vdash \psi \barwedge (\chi \barwedge \chi) \)
Conclusion
\( \vdash \varphi \barwedge (\chi \barwedge \chi) \)
Proof
nic-ich.2
l1
nic-isw1 _
\( \vdash (\chi \barwedge \chi) \barwedge \psi \)
nic-ich.1
\( \vdash \varphi \barwedge (\psi \barwedge \psi) \)
nic-imp _
\( \vdash ((\chi \barwedge \chi) \barwedge \psi) \barwedge ((\varphi \barwedge (\chi \barwedge \chi)) \barwedge (\varphi \barwedge (\chi \barwedge \chi))) \)
nic-mp l1 _