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 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))

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  943  nanbi  1527  rb-bijust  1776  sbnf  2352  sbnf2  2396  sb8mo  2635  raleqbii  3343  rmo5  3394  cbvrmo  3416  sstr2  3952  ss2ab  4023  sbcssg  4487  ssextss  5435  ssrel3  5773  relop  5837  dmcosseq  5969  dmcosseqOLD  5970  intasym  6116  intirr  6119  codir  6121  qfto  6122  cnvpo  6289  dfpo2  6298  dffun2  6547  dff14a  7269  porpss  7725  funcnvuni  7929  poxp  8124  infcllem  9448  ttrclss  9689  cp  9877  aceq2  10103  kmlem12  10145  kmlem15  10148  zfcndpow  10601  grothprim  10819  dfinfre  12196  infrenegsup  12198  xrinfmss2  13337  algcvgblem  16635  isprm2  16740  odulub  18461  oduglb  18463  isirred2  20503  isdomn3  20799  opprdomnb  20801  prmidl0  21447  ntreq0  23203  ist0-3  23471  ist1-3  23475  ordthaus  23510  dfconn2  23545  iscusp2  24427  mdsymlem8  32703  mo5f  32776  iuninc  32846  suppss2f  32924  tosglblem  33235  esumpfinvalf  34411  bnj110  35191  bnj92  35195  bnj539  35224  bnj540  35225  axrepprim  36093  axacprim  36098  dffr5  36145  dfso2  36146  elpotr  36170  mh-setind  36936  regsfromsetind  36939  bj-exexalal  37088  bj-cbvaew  37155  bj-alcomexcom  37192  bj-axseprep  37599  itg2addnclem2  38211  isdmn3  38613  sbcimi  38649  inxpss3  38859  trcoss2  39113  unitscyglem3  42854  eu6w  43300  moxfr  43315  ifpim123g  44118  elmapintrab  44194  undmrnresiss  44222  cnvssco  44224  snhesn  44404  psshepw  44406  frege77  44558  frege93  44574  frege116  44597  frege118  44599  frege131  44612  frege133  44614  ntrneikb  44712  ismnuprim  44896  onfrALTlem5  45143  onfrALTlem5VD  45485  dfac5prim  45591  permaxpow  45610  permac8prim  45615  setis  50361  alsbii  50463  ralsbii  50464