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  2362  sb8mo  2601  raleqbii  3309  rmo5  3360  cbvrmo  3382  sstr2  3928  ss2ab  4001  sbcssg  4461  ssextss  5405  ssrel3  5742  relop  5805  dmcosseq  5933  dmcosseqOLD  5934  dmcosseqOLDOLD  5935  intasym  6078  intirr  6081  codir  6083  qfto  6084  cnvpo  6251  dfpo2  6260  dffun2  6508  dff14a  7225  porpss  7681  funcnvuni  7883  poxp  8078  infcllem  9401  ttrclss  9641  cp  9815  aceq2  10041  kmlem12  10084  kmlem15  10087  zfcndpow  10539  grothprim  10757  dfinfre  12137  infrenegsup  12139  xrinfmss2  13263  algcvgblem  16546  isprm2  16651  odulub  18371  oduglb  18373  isirred2  20401  isdomn2OLD  20689  isdomn3  20692  opprdomnb  20694  ntreq0  23042  ist0-3  23310  ist1-3  23314  ordthaus  23349  dfconn2  23384  iscusp2  24266  mdsymlem8  32481  mo5f  32558  iuninc  32630  suppss2f  32711  tosglblem  33034  prmidl0  33510  esumpfinvalf  34220  bnj110  35000  bnj92  35004  bnj539  35033  bnj540  35034  axrepprim  35884  axacprim  35889  dffr5  35936  dfso2  35937  elpotr  35961  mh-setind  36718  regsfromsetind  36721  bj-exexalal  36871  bj-cbvaew  36938  bj-alcomexcom  36975  bj-axseprep  37381  itg2addnclem2  37993  isdmn3  38395  sbcimi  38431  inxpss3  38641  trcoss2  38895  unitscyglem3  42636  eu6w  43109  moxfr  43124  ifpim123g  43927  elmapintrab  44003  undmrnresiss  44031  cnvssco  44033  snhesn  44213  psshepw  44215  frege77  44367  frege93  44383  frege116  44406  frege118  44408  frege131  44421  frege133  44423  ntrneikb  44521  ismnuprim  44721  onfrALTlem5  44969  onfrALTlem5VD  45311  dfac5prim  45417  permaxpow  45436  permac8prim  45441  setis  50173