Metamath Proof Explorer

Theorem syl5

Description: A syllogism rule of inference. The first premise is used to replace the second antecedent of the second premise. (Contributed by NM, 27-Dec-1992) (Proof shortened by Wolf Lammen, 25-May-2013)

Ref Expression
Hypotheses syl5.1 φ ψ
syl5.2 χ ψ θ
Assertion syl5 χ φ θ


Step Hyp Ref Expression
1 syl5.1 φ ψ
2 syl5.2 χ ψ θ
3 1 2 syl5com φ χ θ
4 3 com12 χ φ θ