Metamath Proof Explorer


Theorem syl3anl1

Description: A syllogism inference. (Contributed by NM, 24-Feb-2005)

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

Proof

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