Metamath Proof Explorer


Theorem imbitrrid

Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994)

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

Proof

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