Theorem imbi12i 239

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  stdcn  848  dcfromcon  1467  dcfrompeirce  1468  nfbii  1495  sbi2v  1915  sbim  1980  sb8mo  2067  cbvmo  2093  necon4ddc  2447  raleqbii  2517  rmo5  2725  cbvrmo  2736  ss2ab  3260  snsssn  3801  trint  4156  ssextss  4263  ordsoexmid  4609  zfregfr  4621  tfi  4629  peano2  4642  peano5  4645  relop  4827  dmcosseq  4949  cotr  5063  issref  5064  cnvsym  5065  intasym  5066  intirr  5068  codir  5070  qfto  5071  cnvpom  5224  cnvsom  5225  funcnvuni  5342  poxp  6317  infmoti  7129  dfinfre  9028  bezoutlembi  12297  algcvgblem  12342  isprm2  12410  ntreq0  14575  ss1oel2o  15890