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  832  nfbii  1449  sbi2v  1864  sbim  1926  sb8mo  2013  cbvmo  2039  necon4ddc  2380  raleqbii  2447  rmo5  2646  cbvrmo  2653  ss2ab  3165  snsssn  3688  trint  4041  ssextss  4142  ordsoexmid  4477  zfregfr  4488  tfi  4496  peano2  4509  peano5  4512  relop  4689  dmcosseq  4810  cotr  4920  issref  4921  cnvsym  4922  intasym  4923  intirr  4925  codir  4927  qfto  4928  cnvpom  5081  cnvsom  5082  funcnvuni  5192  poxp  6129  infmoti  6915  dfinfre  8714  bezoutlembi  11693  algcvgblem  11730  isprm2  11798  ntreq0  12301  ss1oel2o  13189