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 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  929  nanbi  1498  rb-bijust  1751  sbnf2  2354  sb8mo  2594  cbvmowOLD  2597  raleqbii  3313  rmo5  3371  cbvrmowOLD  3386  cbvrmo  3398  ss2ab  4021  sbcssg  4486  ssextss  5415  ssrel3  5747  relop  5811  dmcosseq  5933  cotrgOLDOLD  6068  cnvsymOLDOLD  6073  intasym  6074  intirr  6077  codir  6079  qfto  6080  cnvpo  6244  dfpo2  6253  dffun2  6511  dffun2OLD  6512  dff14a  7222  porpss  7669  funcnvuni  7873  poxp  8065  infcllem  9432  ttrclss  9665  cp  9836  aceq2  10064  kmlem12  10106  kmlem15  10109  zfcndpow  10561  grothprim  10779  dfinfre  12145  infrenegsup  12147  xrinfmss2  13240  algcvgblem  16464  isprm2  16569  odulub  18310  oduglb  18312  isirred2  20146  isdomn2  20806  ntreq0  22465  ist0-3  22733  ist1-3  22737  ordthaus  22772  dfconn2  22807  iscusp2  23691  mdsymlem8  31415  mo5f  31481  iuninc  31546  suppss2f  31620  tosglblem  31904  prmidl0  32299  esumpfinvalf  32764  bnj110  33559  bnj92  33563  bnj539  33592  bnj540  33593  axrepprim  34360  axacprim  34365  dffr5  34413  dfso2  34414  elpotr  34442  bj-alcomexcom  35221  itg2addnclem2  36203  isdmn3  36606  sbcimi  36642  inxpss3  36848  trcoss2  37019  moxfr  41073  isdomn3  41589  ifpim123g  41894  elmapintrab  41970  undmrnresiss  41998  cnvssco  42000  snhesn  42180  psshepw  42182  frege77  42334  frege93  42350  frege116  42373  frege118  42375  frege131  42388  frege133  42390  ntrneikb  42488  ismnuprim  42696  onfrALTlem5  42946  onfrALTlem5VD  43289  setis  47263