Metamath Proof Explorer


Theorem sylan2

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994) (Proof shortened by Wolf Lammen, 22-Nov-2012)

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

Proof

Step Hyp Ref Expression
1 sylan2.1 φ χ
2 sylan2.2 ψ χ θ
3 1 adantl ψ φ χ
4 3 2 syldan ψ φ θ