Theorem imbi12i 238

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 225	. 2 ⊢ ((𝜑 → 𝜒) ↔ (𝜑 → 𝜃))
3		imbi12i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	imbi1i 237	. 2 ⊢ ((𝜑 → 𝜃) ↔ (𝜓 → 𝜃))
5	2, 4	bitri 183	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  stdcn  833  nfbii  1450  sbi2v  1865  sbim  1927  sb8mo  2014  cbvmo  2040  necon4ddc  2381  raleqbii  2450  rmo5  2649  cbvrmo  2656  ss2ab  3170  snsssn  3696  trint  4049  ssextss  4150  ordsoexmid  4485  zfregfr  4496  tfi  4504  peano2  4517  peano5  4520  relop  4697  dmcosseq  4818  cotr  4928  issref  4929  cnvsym  4930  intasym  4931  intirr  4933  codir  4935  qfto  4936  cnvpom  5089  cnvsom  5090  funcnvuni  5200  poxp  6137  infmoti  6923  dfinfre  8738  bezoutlembi  11729  algcvgblem  11766  isprm2  11834  ntreq0  12340  ss1oel2o  13360