Metamath Proof Explorer


Theorem a1dd

Description: Double deduction introducing an antecedent. Deduction associated with a1d . Double deduction associated with ax-1 and a1i . (Contributed by NM, 17-Dec-2004) (Proof shortened by Mel L. O'Cat, 15-Jan-2008)

Ref Expression
Hypothesis a1dd.1 φ ψ χ
Assertion a1dd φ ψ θ χ

Proof

Step Hyp Ref Expression
1 a1dd.1 φ ψ χ
2 ax-1 χ θ χ
3 1 2 syl6 φ ψ θ χ