Metamath Proof Explorer

Theorem bi123imp0

Description: Similar to 3imp except all implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017)

Ref Expression
Hypothesis bi23imp0.1 ⊢ φ ↔ ψ ↔ χ ↔ θ
Assertion bi123imp0 ⊢ φ ∧ ψ ∧ χ → θ

Proof

Step Hyp Ref Expression
1 bi23imp0.1 ⊢ φ ↔ ψ ↔ χ ↔ θ
2 biimp ⊢ ψ ↔ χ ↔ θ → ψ → χ ↔ θ
3 biimp ⊢ χ ↔ θ → χ → θ
4 2 3 syl6 ⊢ ψ ↔ χ ↔ θ → ψ → χ → θ
5 1 4 sylbi ⊢ φ → ψ → χ → θ
6 5 3imp ⊢ φ ∧ ψ ∧ χ → θ