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  2317  sbnf2  2362  sb8mo  2601  raleqbii  3314  rmo5  3368  cbvrmo  3392  sstr2  3940  ss2ab  4013  sbcssg  4474  ssextss  5401  ssrel3  5735  relop  5799  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  intasym  6072  intirr  6075  codir  6077  qfto  6078  cnvpo  6245  dfpo2  6254  dffun2  6502  dff14a  7216  porpss  7672  funcnvuni  7874  poxp  8070  infcllem  9391  ttrclss  9629  cp  9803  aceq2  10029  kmlem12  10072  kmlem15  10075  zfcndpow  10527  grothprim  10745  dfinfre  12123  infrenegsup  12125  xrinfmss2  13226  algcvgblem  16504  isprm2  16609  odulub  18328  oduglb  18330  isirred2  20357  isdomn2OLD  20645  isdomn3  20648  opprdomnb  20650  ntreq0  23021  ist0-3  23289  ist1-3  23293  ordthaus  23328  dfconn2  23363  iscusp2  24245  mdsymlem8  32485  mo5f  32563  iuninc  32635  suppss2f  32716  tosglblem  33056  prmidl0  33531  esumpfinvalf  34233  bnj110  35014  bnj92  35018  bnj539  35047  bnj540  35048  axrepprim  35896  axacprim  35901  dffr5  35948  dfso2  35949  elpotr  35973  mh-setind  36666  regsfromsetind  36669  bj-alcomexcom  36881  itg2addnclem2  37873  isdmn3  38275  sbcimi  38311  inxpss3  38513  trcoss2  38747  unitscyglem3  42451  eu6w  42919  moxfr  42934  ifpim123g  43741  elmapintrab  43817  undmrnresiss  43845  cnvssco  43847  snhesn  44027  psshepw  44029  frege77  44181  frege93  44197  frege116  44220  frege118  44222  frege131  44235  frege133  44237  ntrneikb  44335  ismnuprim  44535  onfrALTlem5  44783  onfrALTlem5VD  45125  dfac5prim  45231  permaxpow  45250  permac8prim  45255  setis  49943