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 205

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 206

This theorem is referenced by:  orimdi  930  nanbi  1499  rb-bijust  1752  sbnf2  2355  sb8mo  2596  cbvmowOLD  2599  raleqbii  3339  sbralie  3355  rmo5  3397  cbvrmowOLD  3412  cbvrmo  3426  ss2ab  4057  sbcssg  4524  ssextss  5454  ssrel3  5787  relop  5851  dmcosseq  5973  cotrgOLDOLD  6111  cnvsymOLDOLD  6116  intasym  6117  intirr  6120  codir  6122  qfto  6123  cnvpo  6287  dfpo2  6296  dffun2  6554  dffun2OLD  6555  dff14a  7269  porpss  7717  funcnvuni  7922  poxp  8114  infcllem  9482  ttrclss  9715  cp  9886  aceq2  10114  kmlem12  10156  kmlem15  10159  zfcndpow  10611  grothprim  10829  dfinfre  12195  infrenegsup  12197  xrinfmss2  13290  algcvgblem  16514  isprm2  16619  odulub  18360  oduglb  18362  isirred2  20235  isdomn2  20915  ntreq0  22581  ist0-3  22849  ist1-3  22853  ordthaus  22888  dfconn2  22923  iscusp2  23807  mdsymlem8  31663  mo5f  31729  iuninc  31792  suppss2f  31863  tosglblem  32144  prmidl0  32569  esumpfinvalf  33074  bnj110  33869  bnj92  33873  bnj539  33902  bnj540  33903  axrepprim  34671  axacprim  34676  dffr5  34724  dfso2  34725  elpotr  34753  bj-alcomexcom  35558  itg2addnclem2  36540  isdmn3  36942  sbcimi  36978  inxpss3  37183  trcoss2  37354  moxfr  41430  isdomn3  41946  ifpim123g  42251  elmapintrab  42327  undmrnresiss  42355  cnvssco  42357  snhesn  42537  psshepw  42539  frege77  42691  frege93  42707  frege116  42730  frege118  42732  frege131  42745  frege133  42747  ntrneikb  42845  ismnuprim  43053  onfrALTlem5  43303  onfrALTlem5VD  43646  setis  47743