Metamath Proof Explorer

Theorem anim1d

Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994)

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


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