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  929  nanbi  1497  rb-bijust  1747  sbnf  2316  sbnf2  2364  sb8mo  2604  raleqbii  3352  rmo5  3408  cbvrmo  3436  sstr2  4015  ss2ab  4085  sbcssg  4543  ssextss  5473  ssrel3  5810  relop  5875  dmcosseq  5999  dmcosseqOLD  6000  cotrgOLDOLD  6141  cnvsymOLDOLD  6146  intasym  6147  intirr  6150  codir  6152  qfto  6153  cnvpo  6318  dfpo2  6327  dffun2  6583  dffun2OLD  6584  dff14a  7307  porpss  7762  funcnvuni  7972  poxp  8169  infcllem  9556  ttrclss  9789  cp  9960  aceq2  10188  kmlem12  10231  kmlem15  10234  zfcndpow  10685  grothprim  10903  dfinfre  12276  infrenegsup  12278  xrinfmss2  13373  algcvgblem  16624  isprm2  16729  odulub  18477  oduglb  18479  isirred2  20447  isdomn2OLD  20734  isdomn3  20737  opprdomnb  20739  ntreq0  23106  ist0-3  23374  ist1-3  23378  ordthaus  23413  dfconn2  23448  iscusp2  24332  mdsymlem8  32442  mo5f  32517  iuninc  32583  suppss2f  32657  tosglblem  32947  prmidl0  33443  esumpfinvalf  34040  bnj110  34834  bnj92  34838  bnj539  34867  bnj540  34868  axrepprim  35664  axacprim  35669  dffr5  35716  dfso2  35717  elpotr  35745  bj-alcomexcom  36646  itg2addnclem2  37632  isdmn3  38034  sbcimi  38070  inxpss3  38270  trcoss2  38440  unitscyglem3  42154  eu6w  42631  moxfr  42648  ifpim123g  43462  elmapintrab  43538  undmrnresiss  43566  cnvssco  43568  snhesn  43748  psshepw  43750  frege77  43902  frege93  43918  frege116  43941  frege118  43943  frege131  43956  frege133  43958  ntrneikb  44056  ismnuprim  44263  onfrALTlem5  44513  onfrALTlem5VD  44856  setis  48790