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  849  dcfromcon  1469  dcfrompeirce  1470  nfbii  1497  sbi2v  1917  sbim  1982  sb8mo  2069  cbvmo  2095  necon4ddc  2449  raleqbii  2519  rmo5  2727  cbvrmo  2738  ss2ab  3265  snsssn  3810  trint  4168  ssextss  4277  ordsoexmid  4623  zfregfr  4635  tfi  4643  peano2  4656  peano5  4659  relop  4841  dmcosseq  4964  cotr  5078  issref  5079  cnvsym  5080  intasym  5081  intirr  5083  codir  5085  qfto  5086  cnvpom  5239  cnvsom  5240  funcnvuni  5357  poxp  6336  infmoti  7151  dfinfre  9059  bezoutlembi  12411  algcvgblem  12456  isprm2  12524  ntreq0  14689  ss1oel2o  16097