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

Metamath Proof Explorer

Theorem syl3anbr

Description: A triple syllogism inference. (Contributed by NM, 29-Dec-2011)

Ref Expression
Hypotheses syl3anbr.1 ⊢ ψ ↔ φ
syl3anbr.2 ⊢ θ ↔ χ
syl3anbr.3 ⊢ η ↔ τ
syl3anbr.4 ⊢ ψ ∧ θ ∧ η → ζ
Assertion syl3anbr ⊢ φ ∧ χ ∧ τ → ζ

Proof

Step Hyp Ref Expression
1 syl3anbr.1 ⊢ ψ ↔ φ
2 syl3anbr.2 ⊢ θ ↔ χ
3 syl3anbr.3 ⊢ η ↔ τ
4 syl3anbr.4 ⊢ ψ ∧ θ ∧ η → ζ
5 1 bicomi ⊢ φ ↔ ψ
6 2 bicomi ⊢ χ ↔ θ
7 3 bicomi ⊢ τ ↔ η
8 5 6 7 4 syl3anb ⊢ φ ∧ χ ∧ τ → ζ