Metamath Proof Explorer


Theorem syl5ibrcom

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

Ref Expression
Hypotheses imbitrrid.1 φ θ
imbitrrid.2 χ ψ θ
Assertion syl5ibrcom φ χ ψ

Proof

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