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 ψφθ