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

Metamath Proof Explorer

Theorem imbi12i

Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 1-Aug-1993)

Ref Expression
Hypotheses imbi12i.1 ⊢ φ ↔ ψ
imbi12i.2 ⊢ χ ↔ θ
Assertion imbi12i ⊢ φ → χ ↔ ψ → θ

Proof

Step Hyp Ref Expression
1 imbi12i.1 ⊢ φ ↔ ψ
2 imbi12i.2 ⊢ χ ↔ θ
3 imbi12 ⊢ φ ↔ ψ → χ ↔ θ → φ → χ ↔ ψ → θ
4 1 2 3 mp2 ⊢ φ → χ ↔ ψ → θ