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  931  nanbi  1500  rb-bijust  1749  sbnf  2312  sbnf2  2361  sb8mo  2601  raleqbii  3344  rmo5  3400  cbvrmo  3429  sstr2  3990  ss2ab  4062  sbcssg  4520  ssextss  5458  ssrel3  5796  relop  5861  dmcosseq  5987  dmcosseqOLD  5988  cotrgOLDOLD  6129  cnvsymOLDOLD  6134  intasym  6135  intirr  6138  codir  6140  qfto  6141  cnvpo  6307  dfpo2  6316  dffun2  6571  dffun2OLD  6572  dff14a  7290  porpss  7747  funcnvuni  7954  poxp  8153  infcllem  9527  ttrclss  9760  cp  9931  aceq2  10159  kmlem12  10202  kmlem15  10205  zfcndpow  10656  grothprim  10874  dfinfre  12249  infrenegsup  12251  xrinfmss2  13353  algcvgblem  16614  isprm2  16719  odulub  18452  oduglb  18454  isirred2  20421  isdomn2OLD  20712  isdomn3  20715  opprdomnb  20717  ntreq0  23085  ist0-3  23353  ist1-3  23357  ordthaus  23392  dfconn2  23427  iscusp2  24311  mdsymlem8  32429  mo5f  32508  iuninc  32573  suppss2f  32648  tosglblem  32964  prmidl0  33478  esumpfinvalf  34077  bnj110  34872  bnj92  34876  bnj539  34905  bnj540  34906  axrepprim  35702  axacprim  35707  dffr5  35754  dfso2  35755  elpotr  35782  bj-alcomexcom  36681  itg2addnclem2  37679  isdmn3  38081  sbcimi  38117  inxpss3  38315  trcoss2  38485  unitscyglem3  42198  eu6w  42686  moxfr  42703  ifpim123g  43513  elmapintrab  43589  undmrnresiss  43617  cnvssco  43619  snhesn  43799  psshepw  43801  frege77  43953  frege93  43969  frege116  43992  frege118  43994  frege131  44007  frege133  44009  ntrneikb  44107  ismnuprim  44313  onfrALTlem5  44562  onfrALTlem5VD  44905  dfac5prim  45007  setis  49217