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

Metamath Proof Explorer

Theorem syl3anb

Description: A triple syllogism inference. (Contributed by NM, 15-Oct-2005)

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

Proof

Step Hyp Ref Expression
1 syl3anb.1 ⊢ φ ↔ ψ
2 syl3anb.2 ⊢ χ ↔ θ
3 syl3anb.3 ⊢ τ ↔ η
4 syl3anb.4 ⊢ ψ ∧ θ ∧ η → ζ
5 1 2 3 3anbi123i ⊢ φ ∧ χ ∧ τ ↔ ψ ∧ θ ∧ η
6 5 4 sylbi ⊢ φ ∧ χ ∧ τ → ζ