Theorem imbi12i 353

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 349	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))
4	1, 2, 3	mp2 9	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  orimdi  944  nanbi  1530  rb-bijust  1782  sbnf  2348  sbnf2  2390  sb8mo  2629  raleqbii  3336  rmo5  3387  cbvrmo  3409  sstr2  3920  ss2ab  3989  sbcssg  4480  ssextss  5428  ssrel3  5771  relop  5838  dmcosseq  5972  dmcosseqOLD  5973  intasym  6127  intirr  6130  codir  6132  qfto  6133  cnvpo  6314  dfpo2  6325  dffun2  6576  dff14a  7305  porpss  7775  funcnvuni  7978  poxp  8177  infcllem  9517  ttrclss  9758  cp  9991  aceq2  10237  kmlem12  10279  kmlem15  10282  zfcndpow  10740  grothprim  10958  dfinfre  12338  infrenegsup  12340  xrinfmss2  13481  algcvgblem  16796  isprm2  16901  odulub  18629  oduglb  18631  isirred2  20702  isdomn3  21017  opprdomnb  21019  prmidl0  21685  ntreq0  23450  ist0-3  23718  ist1-3  23722  ordthaus  23757  dfconn2  23792  iscusp2  24675  mdsymlem8  33069  mo5f  33184  iuninc  33253  suppss2f  33330  tosglblem  33631  esumpfinvalf  34819  bnj110  35599  bnj92  35603  bnj539  35632  bnj540  35633  axrepprim  36682  axacprim  36687  dfso2  36735  elpotr  36758  mh-setind  37539  regsfromsetind  37542  bj-exexalal  37691  bj-cbvaew  37758  bj-alcomexcom  37795  bj-axseprep  38260  itg2addnclem2  38858  isdmn3  39274  sbcimi  39308  inxpss3  39518  trcoss2  39772  unitscyglem3  43513  eu6w  43953  moxfr  43969  ifpim123g  44762  elmapintrab  44838  undmrnresiss  44865  cnvssco  44867  snhesn  45047  psshepw  45049  frege77  45201  frege93  45217  frege116  45240  frege118  45242  frege131  45255  frege133  45257  ntrneikb  45355  ismnuprim  45539  onfrALTlem5  45785  onfrALTlem5VD  46127  dfac5prim  46244  permaxpow  46263  permac8prim  46268  isidom3  49773  setis  51197  alsbii  51324  ralsbii  51325  alseubii  51356  ralseubii  51357