Metamath Proof Explorer

Theorem adantl

Description: Inference adding a conjunct to the left of an antecedent. (Contributed by NM, 30-Aug-1993) (Proof shortened by Wolf Lammen, 23-Nov-2012)

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


Step Hyp Ref Expression
1 adantl.1 φ ψ
2 1 adantr φ χ ψ
3 2 ancoms χ φ ψ