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  3310  rmo5  3361  cbvrmo  3383  sstr2  3929  ss2ab  4002  sbcssg  4462  ssextss  5401  ssrel3  5736  relop  5800  dmcosseq  5928  dmcosseqOLD  5929  dmcosseqOLDOLD  5930  intasym  6073  intirr  6076  codir  6078  qfto  6079  cnvpo  6246  dfpo2  6255  dffun2  6503  dff14a  7219  porpss  7675  funcnvuni  7877  poxp  8072  infcllem  9395  ttrclss  9635  cp  9809  aceq2  10035  kmlem12  10078  kmlem15  10081  zfcndpow  10533  grothprim  10751  dfinfre  12131  infrenegsup  12133  xrinfmss2  13257  algcvgblem  16540  isprm2  16645  odulub  18365  oduglb  18367  isirred2  20395  isdomn2OLD  20683  isdomn3  20686  opprdomnb  20688  ntreq0  23055  ist0-3  23323  ist1-3  23327  ordthaus  23362  dfconn2  23397  iscusp2  24279  mdsymlem8  32499  mo5f  32576  iuninc  32648  suppss2f  32729  tosglblem  33052  prmidl0  33528  esumpfinvalf  34239  bnj110  35019  bnj92  35023  bnj539  35052  bnj540  35053  axrepprim  35903  axacprim  35908  dffr5  35955  dfso2  35956  elpotr  35980  mh-setind  36737  regsfromsetind  36740  bj-exexalal  36890  bj-cbvaew  36957  bj-alcomexcom  36994  bj-axseprep  37400  itg2addnclem2  38010  isdmn3  38412  sbcimi  38448  inxpss3  38658  trcoss2  38912  unitscyglem3  42653  eu6w  43126  moxfr  43141  ifpim123g  43948  elmapintrab  44024  undmrnresiss  44052  cnvssco  44054  snhesn  44234  psshepw  44236  frege77  44388  frege93  44404  frege116  44427  frege118  44429  frege131  44442  frege133  44444  ntrneikb  44542  ismnuprim  44742  onfrALTlem5  44990  onfrALTlem5VD  45332  dfac5prim  45438  permaxpow  45457  permac8prim  45462  setis  50188