Theorem imbi12i 354

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  orimdi  928  nanbi  1491  rb-bijust  1751  sbnf2  2366  sb8mo  2662  cbvmowOLD  2664  raleqbii  3197  rmo5  3379  cbvrmowOLD  3391  cbvrmo  3395  ss2ab  3987  sbcssg  4421  ssextss  5311  relop  5685  dmcosseq  5809  cotrg  5938  cnvsym  5941  intasym  5942  intirr  5945  codir  5947  qfto  5948  cnvpo  6106  dff14a  7006  porpss  7433  funcnvuni  7618  poxp  7805  infcllem  8935  cp  9304  aceq2  9530  kmlem12  9572  kmlem15  9575  zfcndpow  10027  grothprim  10245  dfinfre  11609  infrenegsup  11611  xrinfmss2  12692  algcvgblem  15911  isprm2  16016  oduglb  17741  odulub  17743  isirred2  19447  isdomn2  20065  ntreq0  21682  ist0-3  21950  ist1-3  21954  ordthaus  21989  dfconn2  22024  iscusp2  22908  mdsymlem8  30193  mo5f  30260  iuninc  30324  suppss2f  30398  tosglblem  30682  prmidl0  31034  esumpfinvalf  31445  bnj110  32240  bnj92  32244  bnj539  32273  bnj540  32274  axrepprim  33041  axacprim  33046  dffr5  33102  dfso2  33103  dfpo2  33104  elpotr  33139  bj-alcomexcom  34127  itg2addnclem2  35109  isdmn3  35512  sbcimi  35548  ssrel3  35716  inxpss3  35731  trcoss2  35884  moxfr  39633  isdomn3  40148  ifpim123g  40208  elmapintrab  40276  undmrnresiss  40304  cnvssco  40306  snhesn  40487  psshepw  40489  frege77  40641  frege93  40657  frege116  40680  frege118  40682  frege131  40695  frege133  40697  ntrneikb  40797  ismnuprim  41002  onfrALTlem5  41248  onfrALTlem5VD  41591  setis  45227