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  928  nanbi  1495  rb-bijust  1752  sbnf2  2356  sb8mo  2601  cbvmowOLD  2604  raleqbii  3163  rmo5  3365  cbvrmowOLD  3378  cbvrmo  3382  ss2ab  3993  sbcssg  4454  ssextss  5369  relop  5759  dmcosseq  5882  cotrg  6016  cnvsym  6019  intasym  6020  intirr  6023  codir  6025  qfto  6026  cnvpo  6190  dfpo2  6199  dffun2  6443  dff14a  7143  porpss  7580  funcnvuni  7778  poxp  7969  infcllem  9246  ttrclss  9478  cp  9649  aceq2  9875  kmlem12  9917  kmlem15  9920  zfcndpow  10372  grothprim  10590  dfinfre  11956  infrenegsup  11958  xrinfmss2  13045  algcvgblem  16282  isprm2  16387  odulub  18125  oduglb  18127  isirred2  19943  isdomn2  20570  ntreq0  22228  ist0-3  22496  ist1-3  22500  ordthaus  22535  dfconn2  22570  iscusp2  23454  mdsymlem8  30772  mo5f  30837  iuninc  30900  suppss2f  30974  tosglblem  31252  prmidl0  31626  esumpfinvalf  32044  bnj110  32838  bnj92  32842  bnj539  32871  bnj540  32872  axrepprim  33643  axacprim  33648  dffr5  33721  dfso2  33722  elpotr  33757  bj-alcomexcom  34862  itg2addnclem2  35829  isdmn3  36232  sbcimi  36268  ssrel3  36434  inxpss3  36449  trcoss2  36602  moxfr  40514  isdomn3  41029  ifpim123g  41107  elmapintrab  41184  undmrnresiss  41212  cnvssco  41214  snhesn  41394  psshepw  41396  frege77  41548  frege93  41564  frege116  41587  frege118  41589  frege131  41602  frege133  41604  ntrneikb  41704  ismnuprim  41912  onfrALTlem5  42162  onfrALTlem5VD  42505  setis  46403