# Metamath Proof Explorer

## Theorem animpimp2impd

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

Ref Expression
Hypotheses animpimp2impd.1 ${⊢}\left({\psi }\wedge {\phi }\right)\to \left({\chi }\to \left({\theta }\to {\eta }\right)\right)$
animpimp2impd.2 ${⊢}\left({\psi }\wedge \left({\phi }\wedge {\theta }\right)\right)\to \left({\eta }\to {\tau }\right)$
Assertion animpimp2impd ${⊢}{\phi }\to \left(\left({\psi }\to {\chi }\right)\to \left({\psi }\to \left({\theta }\to {\tau }\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 animpimp2impd.1 ${⊢}\left({\psi }\wedge {\phi }\right)\to \left({\chi }\to \left({\theta }\to {\eta }\right)\right)$
2 animpimp2impd.2 ${⊢}\left({\psi }\wedge \left({\phi }\wedge {\theta }\right)\right)\to \left({\eta }\to {\tau }\right)$
3 2 expr ${⊢}\left({\psi }\wedge {\phi }\right)\to \left({\theta }\to \left({\eta }\to {\tau }\right)\right)$
4 3 a2d ${⊢}\left({\psi }\wedge {\phi }\right)\to \left(\left({\theta }\to {\eta }\right)\to \left({\theta }\to {\tau }\right)\right)$
5 1 4 syld ${⊢}\left({\psi }\wedge {\phi }\right)\to \left({\chi }\to \left({\theta }\to {\tau }\right)\right)$
6 5 expcom ${⊢}{\phi }\to \left({\psi }\to \left({\chi }\to \left({\theta }\to {\tau }\right)\right)\right)$
7 6 a2d ${⊢}{\phi }\to \left(\left({\psi }\to {\chi }\right)\to \left({\psi }\to \left({\theta }\to {\tau }\right)\right)\right)$