Metamath Proof Explorer


Theorem syl6bir

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

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

Proof

Step Hyp Ref Expression
1 syl6bir.1 φ χ ψ
2 syl6bir.2 χ θ
3 1 biimprd φ ψ χ
4 3 2 syl6 φ ψ θ