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  848  nfbii  1484  sbi2v  1904  sbim  1969  sb8mo  2056  cbvmo  2082  necon4ddc  2436  raleqbii  2506  rmo5  2714  cbvrmo  2725  ss2ab  3248  snsssn  3788  trint  4143  ssextss  4250  ordsoexmid  4595  zfregfr  4607  tfi  4615  peano2  4628  peano5  4631  relop  4813  dmcosseq  4934  cotr  5048  issref  5049  cnvsym  5050  intasym  5051  intirr  5053  codir  5055  qfto  5056  cnvpom  5209  cnvsom  5210  funcnvuni  5324  poxp  6287  infmoti  7089  dfinfre  8977  bezoutlembi  12145  algcvgblem  12190  isprm2  12258  ntreq0  14311  ss1oel2o  15554