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  3314  rmo5  3371  cbvrmo  3395  sstr2  3950  ss2ab  4022  sbcssg  4479  ssextss  5408  ssrel3  5740  relop  5804  dmcosseq  5929  dmcosseqOLD  5930  cnvsymOLDOLD  6075  intasym  6076  intirr  6079  codir  6081  qfto  6082  cnvpo  6248  dfpo2  6257  dffun2  6509  dffun2OLD  6510  dff14a  7227  porpss  7683  funcnvuni  7888  poxp  8084  infcllem  9415  ttrclss  9649  cp  9820  aceq2  10048  kmlem12  10091  kmlem15  10094  zfcndpow  10545  grothprim  10763  dfinfre  12140  infrenegsup  12142  xrinfmss2  13247  algcvgblem  16523  isprm2  16628  odulub  18346  oduglb  18348  isirred2  20341  isdomn2OLD  20632  isdomn3  20635  opprdomnb  20637  ntreq0  22997  ist0-3  23265  ist1-3  23269  ordthaus  23304  dfconn2  23339  iscusp2  24222  mdsymlem8  32389  mo5f  32468  iuninc  32539  suppss2f  32612  tosglblem  32946  prmidl0  33414  esumpfinvalf  34059  bnj110  34841  bnj92  34845  bnj539  34874  bnj540  34875  axrepprim  35682  axacprim  35687  dffr5  35734  dfso2  35735  elpotr  35762  bj-alcomexcom  36661  itg2addnclem2  37659  isdmn3  38061  sbcimi  38097  inxpss3  38295  trcoss2  38468  unitscyglem3  42178  eu6w  42657  moxfr  42673  ifpim123g  43482  elmapintrab  43558  undmrnresiss  43586  cnvssco  43588  snhesn  43768  psshepw  43770  frege77  43922  frege93  43938  frege116  43961  frege118  43963  frege131  43976  frege133  43978  ntrneikb  44076  ismnuprim  44276  onfrALTlem5  44525  onfrALTlem5VD  44867  dfac5prim  44973  permaxpow  44992  permac8prim  44997  setis  49680