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  852  dcfromcon  1491  dcfrompeirce  1492  nfbii  1519  sbi2v  1939  sbim  2004  sb8mo  2091  cbvmo  2117  necon4ddc  2472  raleqbii  2542  rmo5  2752  cbvrmo  2764  ss2ab  3292  snsssn  3838  trint  4196  ssextss  4305  ordsoexmid  4653  zfregfr  4665  tfi  4673  peano2  4686  peano5  4689  relop  4871  dmcosseq  4995  cotr  5109  issref  5110  cnvsym  5111  intasym  5112  intirr  5114  codir  5116  qfto  5117  cnvpom  5270  cnvsom  5271  funcnvuni  5389  poxp  6376  infmoti  7191  dfinfre  9099  bezoutlembi  12521  algcvgblem  12566  isprm2  12634  ntreq0  14800  ss1oel2o  16313