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  1468  dcfrompeirce  1469  nfbii  1496  sbi2v  1916  sbim  1981  sb8mo  2068  cbvmo  2094  necon4ddc  2448  raleqbii  2518  rmo5  2726  cbvrmo  2737  ss2ab  3261  snsssn  3802  trint  4157  ssextss  4264  ordsoexmid  4610  zfregfr  4622  tfi  4630  peano2  4643  peano5  4646  relop  4828  dmcosseq  4950  cotr  5064  issref  5065  cnvsym  5066  intasym  5067  intirr  5069  codir  5071  qfto  5072  cnvpom  5225  cnvsom  5226  funcnvuni  5343  poxp  6318  infmoti  7130  dfinfre  9029  bezoutlembi  12326  algcvgblem  12371  isprm2  12439  ntreq0  14604  ss1oel2o  15928