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

Metamath Proof Explorer

Theorem syl2anbr

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999)

Ref Expression
Hypotheses syl2anbr.1 ⊢ ψ ↔ φ
syl2anbr.2 ⊢ χ ↔ τ
syl2anbr.3 ⊢ ψ ∧ χ → θ
Assertion syl2anbr ⊢ φ ∧ τ → θ

Proof

Step Hyp Ref Expression
1 syl2anbr.1 ⊢ ψ ↔ φ
2 syl2anbr.2 ⊢ χ ↔ τ
3 syl2anbr.3 ⊢ ψ ∧ χ → θ
4 1 3 sylanbr ⊢ φ ∧ χ → θ
5 2 4 sylan2br ⊢ φ ∧ τ → θ