Metamath Proof Explorer

Theorem adantr

Description: Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993)

Ref Expression
Hypothesis adantr.1 φ ψ
Assertion adantr φ χ ψ


Step Hyp Ref Expression
1 adantr.1 φ ψ
2 1 a1d φ χ ψ
3 2 imp φ χ ψ