Metamath Proof Explorer

Theorem animpimp2impd

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

Ref Expression
Hypotheses animpimp2impd.1 ⊢ ψ ∧ φ → χ → θ → η
animpimp2impd.2 ⊢ ψ ∧ φ ∧ θ → η → τ
Assertion animpimp2impd ⊢ φ → ψ → χ → ψ → θ → τ

Proof

Step Hyp Ref Expression
1 animpimp2impd.1 ⊢ ψ ∧ φ → χ → θ → η
2 animpimp2impd.2 ⊢ ψ ∧ φ ∧ θ → η → τ
3 2 expr ⊢ ψ ∧ φ → θ → η → τ
4 3 a2d ⊢ ψ ∧ φ → θ → η → θ → τ
5 1 4 syld ⊢ ψ ∧ φ → χ → θ → τ
6 5 expcom ⊢ φ → ψ → χ → θ → τ
7 6 a2d ⊢ φ → ψ → χ → ψ → θ → τ