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  1530  rb-bijust  1782  sbnf  2345  sbnf2  2388  sb8mo  2627  raleqbii  3333  rmo5  3384  cbvrmo  3406  sstr2  3938  ss2ab  4009  sbcssg  4477  ssextss  5421  ssrel3  5762  relop  5828  dmcosseq  5960  dmcosseqOLD  5961  intasym  6109  intirr  6112  codir  6114  qfto  6115  cnvpo  6290  dfpo2  6299  dffun2  6548  dff14a  7274  porpss  7743  funcnvuni  7944  poxp  8140  infcllem  9480  ttrclss  9721  cp  9954  aceq2  10198  kmlem12  10240  kmlem15  10243  zfcndpow  10701  grothprim  10919  dfinfre  12298  infrenegsup  12300  xrinfmss2  13441  algcvgblem  16752  isprm2  16857  odulub  18579  oduglb  18581  isirred2  20651  isdomn3  20966  opprdomnb  20968  prmidl0  21634  ntreq0  23395  ist0-3  23663  ist1-3  23667  ordthaus  23702  dfconn2  23737  iscusp2  24620  mdsymlem8  33012  mo5f  33085  iuninc  33155  suppss2f  33232  tosglblem  33535  esumpfinvalf  34708  bnj110  35488  bnj92  35492  bnj539  35521  bnj540  35522  axrepprim  36467  axacprim  36472  dfso2  36520  elpotr  36543  mh-setind  37324  regsfromsetind  37327  bj-exexalal  37476  bj-cbvaew  37543  bj-alcomexcom  37580  bj-axseprep  37990  itg2addnclem2  38590  isdmn3  39008  sbcimi  39042  inxpss3  39252  trcoss2  39506  unitscyglem3  43247  eu6w  43687  moxfr  43702  ifpim123g  44500  elmapintrab  44576  undmrnresiss  44603  cnvssco  44605  snhesn  44785  psshepw  44787  frege77  44939  frege93  44955  frege116  44978  frege118  44980  frege131  44993  frege133  44995  ntrneikb  45093  ismnuprim  45277  onfrALTlem5  45524  onfrALTlem5VD  45866  dfac5prim  45979  permaxpow  45998  permac8prim  46003  isidom3  49441  setis  50790  alsbii  50895  ralsbii  50896  alseubii  50927  ralseubii  50928