Metamath Proof Explorer

Theorem adantrd

Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994)

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


Step Hyp Ref Expression
1 adantrd.1 φ ψ χ
2 simpl ψ θ ψ
3 2 1 syl5 φ ψ θ χ