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  854  dcfromcon  1493  dcfrompeirce  1494  nfbii  1521  sbi2v  1941  sbim  2006  sb8mo  2093  cbvmo  2119  necon4ddc  2474  raleqbii  2544  rmo5  2754  cbvrmo  2766  ss2ab  3295  snsssn  3844  trint  4202  ssextss  4312  ordsoexmid  4660  zfregfr  4672  tfi  4680  peano2  4693  peano5  4696  relop  4880  dmcosseq  5004  cotr  5118  issref  5119  cnvsym  5120  intasym  5121  intirr  5123  codir  5125  qfto  5126  cnvpom  5279  cnvsom  5280  funcnvuni  5399  poxp  6396  infmoti  7226  dfinfre  9135  bezoutlembi  12575  algcvgblem  12620  isprm2  12688  ntreq0  14855  ss1oel2o  16586