Theorem imp5a

An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) (Proof shortened by Wolf Lammen, 2-Aug-2022.)

Hypothesis

imp5.1

\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \rightarrow \tau \rightarrow \eta \)

Conclusion

\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \wedge \tau \rightarrow \eta \)

Proof

imp5.1

imp5d _

exp31 _