Metamath Proof Explorer

Theorem a1ddd

Description: Triple deduction introducing an antecedent to a wff. Deduction associated with a1dd . Double deduction associated with a1d . Triple deduction associated with ax-1 and a1i . (Contributed by Jeff Hankins, 4-Aug-2009)

Ref Expression
Hypothesis a1ddd.1 φ ψ χ τ
Assertion a1ddd φ ψ χ θ τ


Step Hyp Ref Expression
1 a1ddd.1 φ ψ χ τ
2 ax-1 τ θ τ
3 1 2 syl8 φ ψ χ θ τ