Metamath Proof Explorer

Theorem a1d

Description: Deduction introducing an embedded antecedent. Deduction form of ax-1 and a1i . (Contributed by NM, 5-Jan-1993) (Proof shortened by Stefan Allan, 20-Mar-2006)

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


Step Hyp Ref Expression
1 a1d.1 φ ψ
2 ax-1 ψ χ ψ
3 1 2 syl φ χ ψ