This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem biimtrrdi

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

Ref Expression
Hypotheses biimtrrdi.1 ⊢ φ → χ ↔ ψ
biimtrrdi.2 ⊢ χ → θ
Assertion biimtrrdi ⊢ φ → ψ → θ

Proof

Step Hyp Ref Expression
1 biimtrrdi.1 ⊢ φ → χ ↔ ψ
2 biimtrrdi.2 ⊢ χ → θ
3 1 biimprd ⊢ φ → ψ → χ
4 3 2 syl6 ⊢ φ → ψ → θ