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  dcfromcon  1459  dcfrompeirce  1460  nfbii  1487  sbi2v  1907  sbim  1972  sb8mo  2059  cbvmo  2085  necon4ddc  2439  raleqbii  2509  rmo5  2717  cbvrmo  2728  ss2ab  3252  snsssn  3792  trint  4147  ssextss  4254  ordsoexmid  4599  zfregfr  4611  tfi  4619  peano2  4632  peano5  4635  relop  4817  dmcosseq  4938  cotr  5052  issref  5053  cnvsym  5054  intasym  5055  intirr  5057  codir  5059  qfto  5060  cnvpom  5213  cnvsom  5214  funcnvuni  5328  poxp  6299  infmoti  7103  dfinfre  9000  bezoutlembi  12197  algcvgblem  12242  isprm2  12310  ntreq0  14452  ss1oel2o  15722