Metamath Proof Explorer


Theorem syld

Description: Syllogism deduction. Deduction associated with syl . See conventions for the meaning of "associated deduction" or "deduction form". (Contributed by NM, 5-Aug-1993) (Proof shortened by Mel L. O'Cat, 19-Feb-2008) (Proof shortened by Wolf Lammen, 3-Aug-2012)

Ref Expression
Hypotheses syld.1 φ ψ χ
syld.2 φ χ θ
Assertion syld φ ψ θ

Proof

Step Hyp Ref Expression
1 syld.1 φ ψ χ
2 syld.2 φ χ θ
3 2 a1d φ ψ χ θ
4 1 3 mpdd φ ψ θ