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  1500  rb-bijust  1749  sbnf  2312  sbnf2  2360  sb8mo  2600  raleqbii  3323  rmo5  3379  cbvrmo  3408  sstr2  3965  ss2ab  4037  sbcssg  4495  ssextss  5428  ssrel3  5765  relop  5830  dmcosseq  5956  dmcosseqOLD  5957  cotrgOLDOLD  6098  cnvsymOLDOLD  6103  intasym  6104  intirr  6107  codir  6109  qfto  6110  cnvpo  6276  dfpo2  6285  dffun2  6541  dffun2OLD  6542  dff14a  7263  porpss  7721  funcnvuni  7928  poxp  8127  infcllem  9500  ttrclss  9734  cp  9905  aceq2  10133  kmlem12  10176  kmlem15  10179  zfcndpow  10630  grothprim  10848  dfinfre  12223  infrenegsup  12225  xrinfmss2  13327  algcvgblem  16596  isprm2  16701  odulub  18417  oduglb  18419  isirred2  20381  isdomn2OLD  20672  isdomn3  20675  opprdomnb  20677  ntreq0  23015  ist0-3  23283  ist1-3  23287  ordthaus  23322  dfconn2  23357  iscusp2  24240  mdsymlem8  32391  mo5f  32470  iuninc  32541  suppss2f  32616  tosglblem  32954  prmidl0  33465  esumpfinvalf  34107  bnj110  34889  bnj92  34893  bnj539  34922  bnj540  34923  axrepprim  35719  axacprim  35724  dffr5  35771  dfso2  35772  elpotr  35799  bj-alcomexcom  36698  itg2addnclem2  37696  isdmn3  38098  sbcimi  38134  inxpss3  38332  trcoss2  38502  unitscyglem3  42210  eu6w  42699  moxfr  42715  ifpim123g  43524  elmapintrab  43600  undmrnresiss  43628  cnvssco  43630  snhesn  43810  psshepw  43812  frege77  43964  frege93  43980  frege116  44003  frege118  44005  frege131  44018  frege133  44020  ntrneikb  44118  ismnuprim  44318  onfrALTlem5  44567  onfrALTlem5VD  44909  dfac5prim  45015  permaxpow  45034  setis  49562