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  1499  rb-bijust  1748  sbnf  2311  sbnf2  2359  sb8mo  2599  raleqbii  3327  rmo5  3383  cbvrmo  3412  sstr2  3970  ss2ab  4042  sbcssg  4500  ssextss  5438  ssrel3  5776  relop  5841  dmcosseq  5967  dmcosseqOLD  5968  cotrgOLDOLD  6109  cnvsymOLDOLD  6114  intasym  6115  intirr  6118  codir  6120  qfto  6121  cnvpo  6287  dfpo2  6296  dffun2  6551  dffun2OLD  6552  dff14a  7272  porpss  7729  funcnvuni  7936  poxp  8135  infcllem  9509  ttrclss  9742  cp  9913  aceq2  10141  kmlem12  10184  kmlem15  10187  zfcndpow  10638  grothprim  10856  dfinfre  12231  infrenegsup  12233  xrinfmss2  13335  algcvgblem  16596  isprm2  16701  odulub  18421  oduglb  18423  isirred2  20389  isdomn2OLD  20680  isdomn3  20683  opprdomnb  20685  ntreq0  23031  ist0-3  23299  ist1-3  23303  ordthaus  23338  dfconn2  23373  iscusp2  24256  mdsymlem8  32357  mo5f  32436  iuninc  32508  suppss2f  32583  tosglblem  32903  prmidl0  33413  esumpfinvalf  34036  bnj110  34831  bnj92  34835  bnj539  34864  bnj540  34865  axrepprim  35661  axacprim  35666  dffr5  35713  dfso2  35714  elpotr  35741  bj-alcomexcom  36640  itg2addnclem2  37638  isdmn3  38040  sbcimi  38076  inxpss3  38274  trcoss2  38444  unitscyglem3  42157  eu6w  42649  moxfr  42666  ifpim123g  43475  elmapintrab  43551  undmrnresiss  43579  cnvssco  43581  snhesn  43761  psshepw  43763  frege77  43915  frege93  43931  frege116  43954  frege118  43956  frege131  43969  frege133  43971  ntrneikb  44069  ismnuprim  44270  onfrALTlem5  44519  onfrALTlem5VD  44862  dfac5prim  44964  setis  49225