Metamath Proof Explorer


Theorem sylanl1

Description: A syllogism inference. (Contributed by NM, 10-Mar-2005)

Ref Expression
Hypotheses sylanl1.1 φ ψ
sylanl1.2 ψ χ θ τ
Assertion sylanl1 φ χ θ τ

Proof

Step Hyp Ref Expression
1 sylanl1.1 φ ψ
2 sylanl1.2 ψ χ θ τ
3 1 anim1i φ χ ψ χ
4 3 2 sylan φ χ θ τ