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  2356  sb8mo  2594  raleqbii  3317  rmo5  3374  cbvrmo  3398  sstr2  3953  ss2ab  4025  sbcssg  4483  ssextss  5413  ssrel3  5749  relop  5814  dmcosseq  5940  dmcosseqOLD  5941  cotrgOLDOLD  6082  cnvsymOLDOLD  6087  intasym  6088  intirr  6091  codir  6093  qfto  6094  cnvpo  6260  dfpo2  6269  dffun2  6521  dffun2OLD  6522  dff14a  7245  porpss  7703  funcnvuni  7908  poxp  8107  infcllem  9439  ttrclss  9673  cp  9844  aceq2  10072  kmlem12  10115  kmlem15  10118  zfcndpow  10569  grothprim  10787  dfinfre  12164  infrenegsup  12166  xrinfmss2  13271  algcvgblem  16547  isprm2  16652  odulub  18366  oduglb  18368  isirred2  20330  isdomn2OLD  20621  isdomn3  20624  opprdomnb  20626  ntreq0  22964  ist0-3  23232  ist1-3  23236  ordthaus  23271  dfconn2  23306  iscusp2  24189  mdsymlem8  32339  mo5f  32418  iuninc  32489  suppss2f  32562  tosglblem  32900  prmidl0  33421  esumpfinvalf  34066  bnj110  34848  bnj92  34852  bnj539  34881  bnj540  34882  axrepprim  35689  axacprim  35694  dffr5  35741  dfso2  35742  elpotr  35769  bj-alcomexcom  36668  itg2addnclem2  37666  isdmn3  38068  sbcimi  38104  inxpss3  38302  trcoss2  38475  unitscyglem3  42185  eu6w  42664  moxfr  42680  ifpim123g  43489  elmapintrab  43565  undmrnresiss  43593  cnvssco  43595  snhesn  43775  psshepw  43777  frege77  43929  frege93  43945  frege116  43968  frege118  43970  frege131  43983  frege133  43985  ntrneikb  44083  ismnuprim  44283  onfrALTlem5  44532  onfrALTlem5VD  44874  dfac5prim  44980  permaxpow  44999  permac8prim  45004  setis  49687