Metamath Proof Explorer


Theorem imim12d

Description: Deduction combining antecedents and consequents. Deduction associated with imim12 and imim12i . (Contributed by NM, 7-Aug-1994) (Proof shortened by Mel L. O'Cat, 30-Oct-2011)

Ref Expression
Hypotheses imim12d.1 φ ψ χ
imim12d.2 φ θ τ
Assertion imim12d φ χ θ ψ τ

Proof

Step Hyp Ref Expression
1 imim12d.1 φ ψ χ
2 imim12d.2 φ θ τ
3 2 imim2d φ χ θ χ τ
4 1 3 syl5d φ χ θ ψ τ