Metamath Proof Explorer

Theorem anim2d

Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993)

Ref Expression
Hypothesis anim1d.1 φ ψ χ
Assertion anim2d φ θ ψ θ χ


Step Hyp Ref Expression
1 anim1d.1 φ ψ χ
2 idd φ θ θ
3 2 1 anim12d φ θ ψ θ χ