Metamath Proof Explorer

Theorem ancld

Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994) (Proof shortened by Wolf Lammen, 1-Nov-2012)

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


Step Hyp Ref Expression
1 ancld.1 φ ψ χ
2 idd φ ψ ψ
3 2 1 jcad φ ψ ψ χ