Metamath Proof Explorer


Theorem imbitrid

Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993)

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

Proof

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