Metamath Proof Explorer


Theorem syl5ibcom

Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007)

Ref Expression
Hypotheses imbitrid.1 φ ψ
imbitrid.2 χ ψ θ
Assertion syl5ibcom φ χ θ

Proof

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