Theorem animpimp2impd

Deduction deriving nested implications from conjunctions. (Contributed by AV, 21-Aug-2022.)

Hypotheses
animpimp2impd.1
\( \vdash \psi \wedge \varphi \rightarrow \chi \rightarrow \theta \rightarrow \eta \)
animpimp2impd.2
\( \vdash \psi \wedge (\varphi \wedge \theta) \rightarrow \eta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \rightarrow \chi) \rightarrow \psi \rightarrow \theta \rightarrow \tau \)
Proof
l0
animpimp2impd.1
\( \vdash \psi \wedge \varphi \rightarrow \chi \rightarrow \theta \rightarrow \eta \)
animpimp2impd.2
expr _
a2d _
\( \vdash \psi \wedge \varphi \rightarrow (\theta \rightarrow \eta) \rightarrow \theta \rightarrow \tau \)
syld l0 _
expcom _
a2d _