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 φχθτ