Theorem exp4a

An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2021.)

Hypothesis

exp4a.1

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

Conclusion

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

Proof

exp4a.1

imp _

exp4b _