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 ⊢φ∧θ∧η→ψ↔ζ