Metamath Proof Explorer


Theorem sylanr1

Description: A syllogism inference. (Contributed by NM, 9-Apr-2005)

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

Proof

Step Hyp Ref Expression
1 sylanr1.1 φχ
2 sylanr1.2 ψχθτ
3 1 anim1i φθχθ
4 3 2 sylan2 ψφθτ