Theorem a2and

Deduction distributing a conjunction as embedded antecedent. (Contributed by AV, 25-Oct-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)

Hypotheses
a2and.1
\( \vdash \varphi \rightarrow \psi \wedge \rho \rightarrow \tau \rightarrow \theta \)
a2and.2
\( \vdash \varphi \rightarrow \psi \wedge \rho \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \wedge \chi \rightarrow \tau) \rightarrow \psi \wedge \rho \rightarrow \theta \)
Proof
l0
a2and.1
\( \vdash \varphi \rightarrow \psi \wedge \rho \rightarrow \tau \rightarrow \theta \)
a2and.2
expd _
l3
imdistand _
\( \vdash \varphi \rightarrow \psi \wedge \rho \rightarrow \psi \wedge \chi \)
imim1
com3l _
\( \vdash (\tau \rightarrow \theta) \rightarrow \psi \wedge \chi \rightarrow (\psi \wedge \chi \rightarrow \tau) \rightarrow \theta \)
syl6c l0 l3 _
com23 _