Metamath Proof Explorer

Theorem imim2d

Description: Deduction adding nested antecedents. Deduction associated with imim2 and imim2i . (Contributed by NM, 10-Jan-1993)

Ref Expression
Hypothesis imim2d.1 φ ψ χ
Assertion imim2d φ θ ψ θ χ


Step Hyp Ref Expression
1 imim2d.1 φ ψ χ
2 1 a1d φ θ ψ χ
3 2 a2d φ θ ψ θ χ