Theorem a2i

Inference distributing an antecedent. Inference associated with [ax-2]. Its associated inference is mpd. (Contributed by NM, 29-Dec-1992.)

Hypothesis
a2i.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
Proof
l0
a2i.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
ax-2
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l0 _