Theorem imbi12i 237

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 224	. 2 ⊢ ((𝜑 → 𝜒) ↔ (𝜑 → 𝜃))
3		imbi12i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	imbi1i 236	. 2 ⊢ ((𝜑 → 𝜃) ↔ (𝜓 → 𝜃))
5	2, 4	bitri 182	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  nfbii  1407  sbi2v  1820  sbim  1875  sb8mo  1962  cbvmo  1988  necon4ddc  2327  raleqbii  2390  rmo5  2582  cbvrmo  2589  ss2ab  3089  snsssn  3605  trint  3951  ssextss  4047  ordsoexmid  4378  zfregfr  4389  tfi  4397  peano2  4410  peano5  4413  relop  4586  dmcosseq  4704  cotr  4813  issref  4814  cnvsym  4815  intasym  4816  intirr  4818  codir  4820  qfto  4821  cnvpom  4973  cnvsom  4974  funcnvuni  5083  poxp  5997  infmoti  6721  dfinfre  8415  bezoutlembi  11268  algcvgblem  11305  isprm2  11373  ss1oel2o  11843