Metamath Proof Explorer

Theorem imbi13

Description: Join three logical equivalences to form equivalence of implications. imbi13 is imbi13VD without virtual deductions and was automatically derived from imbi13VD using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion imbi13 ⊢ φ ↔ ψ → χ ↔ θ → τ ↔ η → φ → χ → τ ↔ ψ → θ → η

Proof

Step Hyp Ref Expression
1 imbi12 ⊢ χ ↔ θ → τ ↔ η → χ → τ ↔ θ → η
2 imbi12 ⊢ φ ↔ ψ → χ → τ ↔ θ → η → φ → χ → τ ↔ ψ → θ → η
3 1 2 syl9r ⊢ φ ↔ ψ → χ ↔ θ → τ ↔ η → φ → χ → τ ↔ ψ → θ → η