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  1500  rb-bijust  1749  sbnf  2311  sbnf2  2357  sb8mo  2595  raleqbii  3319  rmo5  3376  cbvrmo  3401  sstr2  3956  ss2ab  4028  sbcssg  4486  ssextss  5416  ssrel3  5752  relop  5817  dmcosseq  5943  dmcosseqOLD  5944  cotrgOLDOLD  6085  cnvsymOLDOLD  6090  intasym  6091  intirr  6094  codir  6096  qfto  6097  cnvpo  6263  dfpo2  6272  dffun2  6524  dffun2OLD  6525  dff14a  7248  porpss  7706  funcnvuni  7911  poxp  8110  infcllem  9446  ttrclss  9680  cp  9851  aceq2  10079  kmlem12  10122  kmlem15  10125  zfcndpow  10576  grothprim  10794  dfinfre  12171  infrenegsup  12173  xrinfmss2  13278  algcvgblem  16554  isprm2  16659  odulub  18373  oduglb  18375  isirred2  20337  isdomn2OLD  20628  isdomn3  20631  opprdomnb  20633  ntreq0  22971  ist0-3  23239  ist1-3  23243  ordthaus  23278  dfconn2  23313  iscusp2  24196  mdsymlem8  32346  mo5f  32425  iuninc  32496  suppss2f  32569  tosglblem  32907  prmidl0  33428  esumpfinvalf  34073  bnj110  34855  bnj92  34859  bnj539  34888  bnj540  34889  axrepprim  35696  axacprim  35701  dffr5  35748  dfso2  35749  elpotr  35776  bj-alcomexcom  36675  itg2addnclem2  37673  isdmn3  38075  sbcimi  38111  inxpss3  38309  trcoss2  38482  unitscyglem3  42192  eu6w  42671  moxfr  42687  ifpim123g  43496  elmapintrab  43572  undmrnresiss  43600  cnvssco  43602  snhesn  43782  psshepw  43784  frege77  43936  frege93  43952  frege116  43975  frege118  43977  frege131  43990  frege133  43992  ntrneikb  44090  ismnuprim  44290  onfrALTlem5  44539  onfrALTlem5VD  44881  dfac5prim  44987  permaxpow  45006  permac8prim  45011  setis  49691