Theorem imbi12i 350

Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 1-Aug-1993.)

Hypotheses

Ref	Expression
imbi12i.1	⊢ (𝜑 ↔ 𝜓)
imbi12i.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
imbi12i	⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))

Proof of Theorem imbi12i

Step	Hyp	Ref	Expression
1		imbi12i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		imbi12i.2	. 2 ⊢ (𝜒 ↔ 𝜃)
3		imbi12 346	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))
4	1, 2, 3	mp2 9	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  orimdi  930  nanbi  1501  rb-bijust  1750  sbnf  2313  sbnf2  2358  sb8mo  2596  raleqbii  3310  rmo5  3364  cbvrmo  3388  sstr2  3936  ss2ab  4008  sbcssg  4467  ssextss  5392  ssrel3  5725  relop  5789  dmcosseq  5916  dmcosseqOLD  5917  dmcosseqOLDOLD  5918  intasym  6061  intirr  6064  codir  6066  qfto  6067  cnvpo  6234  dfpo2  6243  dffun2  6491  dff14a  7204  porpss  7660  funcnvuni  7862  poxp  8058  infcllem  9372  ttrclss  9610  cp  9784  aceq2  10010  kmlem12  10053  kmlem15  10056  zfcndpow  10507  grothprim  10725  dfinfre  12103  infrenegsup  12105  xrinfmss2  13210  algcvgblem  16488  isprm2  16593  odulub  18311  oduglb  18313  isirred2  20339  isdomn2OLD  20627  isdomn3  20630  opprdomnb  20632  ntreq0  22992  ist0-3  23260  ist1-3  23264  ordthaus  23299  dfconn2  23334  iscusp2  24216  mdsymlem8  32390  mo5f  32468  iuninc  32540  suppss2f  32620  tosglblem  32955  prmidl0  33415  esumpfinvalf  34089  bnj110  34870  bnj92  34874  bnj539  34903  bnj540  34904  axrepprim  35746  axacprim  35751  dffr5  35798  dfso2  35799  elpotr  35823  bj-alcomexcom  36724  itg2addnclem2  37722  isdmn3  38124  sbcimi  38160  inxpss3  38362  trcoss2  38596  unitscyglem3  42300  eu6w  42779  moxfr  42795  ifpim123g  43603  elmapintrab  43679  undmrnresiss  43707  cnvssco  43709  snhesn  43889  psshepw  43891  frege77  44043  frege93  44059  frege116  44082  frege118  44084  frege131  44097  frege133  44099  ntrneikb  44197  ismnuprim  44397  onfrALTlem5  44645  onfrALTlem5VD  44987  dfac5prim  45093  permaxpow  45112  permac8prim  45117  setis  49809