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

Metamath Proof Explorer

Theorem sylanbr

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

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

Proof

Step Hyp Ref Expression
1 sylanbr.1 ⊢ ψ ↔ φ
2 sylanbr.2 ⊢ ψ ∧ χ → θ
3 1 biimpri ⊢ φ → ψ
4 3 2 sylan ⊢ φ ∧ χ → θ