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  855  dcfromcon  1494  dcfrompeirce  1495  nfbii  1522  sbi2v  1941  sbim  2006  sb8mo  2093  cbvmo  2119  necon4ddc  2475  raleqbii  2545  rmo5  2755  cbvrmo  2767  ss2ab  3296  snsssn  3849  trint  4207  ssextss  4318  ordsoexmid  4666  zfregfr  4678  tfi  4686  peano2  4699  peano5  4702  relop  4886  dmcosseq  5010  cotr  5125  issref  5126  cnvsym  5127  intasym  5128  intirr  5130  codir  5132  qfto  5133  cnvpom  5286  cnvsom  5287  funcnvuni  5406  poxp  6406  infmoti  7270  dfinfre  9178  bezoutlembi  12639  algcvgblem  12684  isprm2  12752  ntreq0  14926  ss1oel2o  16690