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  931  nanbi  1502  rb-bijust  1751  sbnf  2318  sbnf2  2363  sb8mo  2602  raleqbii  3316  rmo5  3370  cbvrmo  3394  sstr2  3942  ss2ab  4015  sbcssg  4476  ssextss  5408  ssrel3  5743  relop  5807  dmcosseq  5935  dmcosseqOLD  5936  dmcosseqOLDOLD  5937  intasym  6080  intirr  6083  codir  6085  qfto  6086  cnvpo  6253  dfpo2  6262  dffun2  6510  dff14a  7226  porpss  7682  funcnvuni  7884  poxp  8080  infcllem  9403  ttrclss  9641  cp  9815  aceq2  10041  kmlem12  10084  kmlem15  10087  zfcndpow  10539  grothprim  10757  dfinfre  12135  infrenegsup  12137  xrinfmss2  13238  algcvgblem  16516  isprm2  16621  odulub  18340  oduglb  18342  isirred2  20369  isdomn2OLD  20657  isdomn3  20660  opprdomnb  20662  ntreq0  23033  ist0-3  23301  ist1-3  23305  ordthaus  23340  dfconn2  23375  iscusp2  24257  mdsymlem8  32498  mo5f  32575  iuninc  32647  suppss2f  32728  tosglblem  33067  prmidl0  33543  esumpfinvalf  34254  bnj110  35034  bnj92  35038  bnj539  35067  bnj540  35068  axrepprim  35918  axacprim  35923  dffr5  35970  dfso2  35971  elpotr  35995  mh-setind  36688  regsfromsetind  36691  bj-exexalal  36831  bj-cbvaew  36887  bj-alcomexcom  36925  bj-axseprep  37322  itg2addnclem2  37923  isdmn3  38325  sbcimi  38361  inxpss3  38571  trcoss2  38825  unitscyglem3  42567  eu6w  43034  moxfr  43049  ifpim123g  43856  elmapintrab  43932  undmrnresiss  43960  cnvssco  43962  snhesn  44142  psshepw  44144  frege77  44296  frege93  44312  frege116  44335  frege118  44337  frege131  44350  frege133  44352  ntrneikb  44450  ismnuprim  44650  onfrALTlem5  44898  onfrALTlem5VD  45240  dfac5prim  45346  permaxpow  45365  permac8prim  45370  setis  50057