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 ⊢ ( ( 𝜑 → 𝜒 ) ↔ ( 𝜓 → 𝜃 ) )