Metamath Proof Explorer


Theorem sylanbr

Description: A syllogism inference. (Contributed by NM, 18-May-1994)

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

Proof

Step Hyp Ref Expression
1 sylanbr.1 ψ φ
2 sylanbr.2 ψ χ θ
3 1 biimpri φ ψ
4 3 2 sylan φ χ θ