Theorem imbi12i 316

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

Hypotheses

Ref	Expression
imbi12i.1	⊢ (φ ↔ ψ)
imbi12i.2	⊢ (χ ↔ θ)

Assertion

Ref	Expression
imbi12i	⊢ ((φ → χ) ↔ (ψ → θ))

Proof of Theorem imbi12i

Step	Hyp	Ref	Expression
1		imbi12i.2	. . 3 ⊢ (χ ↔ θ)
2	1	imbi2i 303	. 2 ⊢ ((φ → χ) ↔ (φ → θ))
3		imbi12i.1	. . 3 ⊢ (φ ↔ ψ)
4	3	imbi1i 315	. 2 ⊢ ((φ → θ) ↔ (ψ → θ))
5	2, 4	bitri 240	1 ⊢ ((φ → χ) ↔ (ψ → θ))

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  orimdi  820  rb-bijust  1514  nfbii  1569  sb8mo  2223  cbvmo  2241  raleqbii  2644  rmo5  2827  cbvrmo  2834  ss2ab  3334  sscon34  3661  evenodddisjlem1  4515  tfinnn  4534  cotr  5026  cnvsym  5027  intasym  5028  intirr  5029  dffun2  5119  funcnvuni  5161  fvfullfunlem1  5861  clos1induct  5880