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  3293  snsssn  3842  trint  4200  ssextss  4310  ordsoexmid  4658  zfregfr  4670  tfi  4678  peano2  4691  peano5  4694  relop  4878  dmcosseq  5002  cotr  5116  issref  5117  cnvsym  5118  intasym  5119  intirr  5121  codir  5123  qfto  5124  cnvpom  5277  cnvsom  5278  funcnvuni  5396  poxp  6392  infmoti  7218  dfinfre  9126  bezoutlembi  12566  algcvgblem  12611  isprm2  12679  ntreq0  14846  ss1oel2o  16522