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  930  nanbi  1501  rb-bijust  1750  sbnf  2315  sbnf2  2360  sb8mo  2599  raleqbii  3312  rmo5  3366  cbvrmo  3390  sstr2  3938  ss2abim  4010  ss2ab  4011  sbcssg  4472  ssextss  5399  ssrel3  5733  relop  5797  dmcosseq  5925  dmcosseqOLD  5926  dmcosseqOLDOLD  5927  intasym  6070  intirr  6073  codir  6075  qfto  6076  cnvpo  6243  dfpo2  6252  dffun2  6500  dff14a  7214  porpss  7670  funcnvuni  7872  poxp  8068  infcllem  9389  ttrclss  9627  cp  9801  aceq2  10027  kmlem12  10070  kmlem15  10073  zfcndpow  10525  grothprim  10743  dfinfre  12121  infrenegsup  12123  xrinfmss2  13224  algcvgblem  16502  isprm2  16607  odulub  18326  oduglb  18328  isirred2  20355  isdomn2OLD  20643  isdomn3  20646  opprdomnb  20648  ntreq0  23019  ist0-3  23287  ist1-3  23291  ordthaus  23326  dfconn2  23361  iscusp2  24243  mdsymlem8  32434  mo5f  32512  iuninc  32584  suppss2f  32665  tosglblem  33005  prmidl0  33480  esumpfinvalf  34182  bnj110  34963  bnj92  34967  bnj539  34996  bnj540  34997  axrepprim  35845  axacprim  35850  dffr5  35897  dfso2  35898  elpotr  35922  bj-alcomexcom  36824  itg2addnclem2  37812  isdmn3  38214  sbcimi  38250  inxpss3  38452  trcoss2  38686  unitscyglem3  42390  eu6w  42861  moxfr  42876  ifpim123g  43683  elmapintrab  43759  undmrnresiss  43787  cnvssco  43789  snhesn  43969  psshepw  43971  frege77  44123  frege93  44139  frege116  44162  frege118  44164  frege131  44177  frege133  44179  ntrneikb  44277  ismnuprim  44477  onfrALTlem5  44725  onfrALTlem5VD  45067  dfac5prim  45173  permaxpow  45192  permac8prim  45197  setis  49885