Theorem imbi12i 353

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  orimdi  944  nanbi  1529  rb-bijust  1781  sbnf  2344  sbnf2  2387  sb8mo  2626  raleqbii  3332  rmo5  3383  cbvrmo  3405  sstr2  3916  ss2ab  3985  sbcssg  4476  ssextss  5421  ssrel3  5763  relop  5829  dmcosseq  5961  dmcosseqOLD  5962  intasym  6111  intirr  6114  codir  6116  qfto  6117  cnvpo  6293  dfpo2  6302  dffun2  6553  dff14a  7278  porpss  7747  funcnvuni  7948  poxp  8147  infcllem  9487  ttrclss  9728  cp  9961  aceq2  10205  kmlem12  10247  kmlem15  10250  zfcndpow  10708  grothprim  10926  dfinfre  12305  infrenegsup  12307  xrinfmss2  13448  algcvgblem  16761  isprm2  16866  odulub  18588  oduglb  18590  isirred2  20660  isdomn3  20975  opprdomnb  20977  prmidl0  21643  ntreq0  23404  ist0-3  23672  ist1-3  23676  ordthaus  23711  dfconn2  23746  iscusp2  24629  mdsymlem8  33021  mo5f  33136  iuninc  33206  suppss2f  33283  tosglblem  33585  esumpfinvalf  34758  bnj110  35538  bnj92  35542  bnj539  35571  bnj540  35572  axrepprim  36591  axacprim  36596  dfso2  36644  elpotr  36667  mh-setind  37448  regsfromsetind  37451  bj-exexalal  37600  bj-cbvaew  37667  bj-alcomexcom  37704  bj-axseprep  38126  itg2addnclem2  38727  isdmn3  39145  sbcimi  39179  inxpss3  39389  trcoss2  39643  unitscyglem3  43384  eu6w  43824  moxfr  43840  ifpim123g  44638  elmapintrab  44714  undmrnresiss  44741  cnvssco  44743  snhesn  44923  psshepw  44925  frege77  45077  frege93  45093  frege116  45116  frege118  45118  frege131  45131  frege133  45133  ntrneikb  45231  ismnuprim  45415  onfrALTlem5  45661  onfrALTlem5VD  46003  dfac5prim  46116  permaxpow  46135  permac8prim  46140  isidom3  49578  setis  51002  alsbii  51107  ralsbii  51108  alseubii  51139  ralseubii  51140