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)$$