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  1942  sbim  2007  sb8mo  2094  cbvmo  2120  necon4ddc  2484  raleqbii  2554  rmo5  2765  cbvrmo  2777  ss2ab  3306  snsssn  3865  trint  4223  ssextss  4336  ordsoexmid  4684  zfregfr  4696  tfi  4704  peano2  4717  peano5  4720  relop  4905  dmcosseq  5029  cotr  5144  issref  5145  cnvsym  5146  intasym  5147  intirr  5149  codir  5151  qfto  5152  cnvpom  5305  cnvsom  5306  funcnvuni  5425  poxp  6428  infmoti  7319  dfinfre  9230  bezoutlembi  12701  algcvgblem  12746  isprm2  12814  ntreq0  14997  ss1oel2o  16761