Metamath Proof Explorer


Theorem syld3an1

Description: A syllogism inference. (Contributed by NM, 7-Jul-2008) (Proof shortened by Wolf Lammen, 26-Jun-2022)

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

Proof

Step Hyp Ref Expression
1 syld3an1.1 χψθφ
2 syld3an1.2 φψθτ
3 simp2 χψθψ
4 simp3 χψθθ
5 1 3 4 2 syl3anc χψθτ