Metamath Proof Explorer

Theorem syl3an9b

Description: Nested syllogism inference conjoining 3 dissimilar antecedents. (Contributed by NM, 1-May-1995)

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

Proof

Step Hyp Ref Expression
1 syl3an9b.1 ⊢ φ → ψ ↔ χ
2 syl3an9b.2 ⊢ θ → χ ↔ τ
3 syl3an9b.3 ⊢ η → τ ↔ ζ
4 1 2 sylan9bb ⊢ φ ∧ θ → ψ ↔ τ
5 4 3 sylan9bb ⊢ φ ∧ θ ∧ η → ψ ↔ ζ
6 5 3impa ⊢ φ ∧ θ ∧ η → ψ ↔ ζ