Metamath Proof Explorer

Theorem ancrd

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

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


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