Theorem imbi12i 351

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 347	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))
4	1, 2, 3	mp2 9	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  orimdi  936  nanbi  1507  rb-bijust  1756  sbnf  2322  sbnf2  2366  sb8mo  2605  raleqbii  3311  rmo5  3362  cbvrmo  3384  sstr2  3922  ss2ab  3992  sbcssg  4449  ssextss  5392  ssrel3  5729  relop  5792  dmcosseq  5920  dmcosseqOLD  5921  dmcosseqOLDOLD  5922  intasym  6065  intirr  6068  codir  6070  qfto  6071  cnvpo  6238  dfpo2  6247  dffun2  6495  dff14a  7214  porpss  7670  funcnvuni  7872  poxp  8068  infcllem  9391  ttrclss  9632  cp  9806  aceq2  10032  kmlem12  10075  kmlem15  10078  zfcndpow  10530  grothprim  10748  dfinfre  12128  infrenegsup  12130  xrinfmss2  13254  algcvgblem  16537  isprm2  16642  odulub  18362  oduglb  18364  isirred2  20392  isdomn2OLD  20684  isdomn3  20687  opprdomnb  20689  ntreq0  23060  ist0-3  23328  ist1-3  23332  ordthaus  23367  dfconn2  23402  iscusp2  24284  mdsymlem8  32499  mo5f  32576  iuninc  32649  suppss2f  32730  tosglblem  33053  prmidl0  33533  esumpfinvalf  34260  bnj110  35040  bnj92  35044  bnj539  35073  bnj540  35074  axrepprim  35930  axacprim  35935  dffr5  35982  dfso2  35983  elpotr  36007  mh-setind  36764  regsfromsetind  36767  bj-exexalal  36917  bj-cbvaew  36984  bj-alcomexcom  37021  bj-axseprep  37427  itg2addnclem2  38039  isdmn3  38441  sbcimi  38477  inxpss3  38687  trcoss2  38941  unitscyglem3  42682  eu6w  43126  moxfr  43141  ifpim123g  43944  elmapintrab  44020  undmrnresiss  44048  cnvssco  44050  snhesn  44230  psshepw  44232  frege77  44384  frege93  44400  frege116  44423  frege118  44425  frege131  44438  frege133  44440  ntrneikb  44538  ismnuprim  44738  onfrALTlem5  44986  onfrALTlem5VD  45328  dfac5prim  45434  permaxpow  45453  permac8prim  45458  setis  50188