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  2311  sbnf2  2356  sb8mo  2594  raleqbii  3314  rmo5  3371  cbvrmo  3395  sstr2  3950  ss2ab  4022  sbcssg  4479  ssextss  5408  ssrel3  5740  relop  5804  dmcosseq  5929  dmcosseqOLD  5930  cnvsymOLDOLD  6075  intasym  6076  intirr  6079  codir  6081  qfto  6082  cnvpo  6248  dfpo2  6257  dffun2  6509  dffun2OLD  6510  dff14a  7227  porpss  7683  funcnvuni  7888  poxp  8084  infcllem  9415  ttrclss  9649  cp  9820  aceq2  10048  kmlem12  10091  kmlem15  10094  zfcndpow  10545  grothprim  10763  dfinfre  12140  infrenegsup  12142  xrinfmss2  13247  algcvgblem  16523  isprm2  16628  odulub  18342  oduglb  18344  isirred2  20306  isdomn2OLD  20597  isdomn3  20600  opprdomnb  20602  ntreq0  22940  ist0-3  23208  ist1-3  23212  ordthaus  23247  dfconn2  23282  iscusp2  24165  mdsymlem8  32312  mo5f  32391  iuninc  32462  suppss2f  32535  tosglblem  32873  prmidl0  33394  esumpfinvalf  34039  bnj110  34821  bnj92  34825  bnj539  34854  bnj540  34855  axrepprim  35662  axacprim  35667  dffr5  35714  dfso2  35715  elpotr  35742  bj-alcomexcom  36641  itg2addnclem2  37639  isdmn3  38041  sbcimi  38077  inxpss3  38275  trcoss2  38448  unitscyglem3  42158  eu6w  42637  moxfr  42653  ifpim123g  43462  elmapintrab  43538  undmrnresiss  43566  cnvssco  43568  snhesn  43748  psshepw  43750  frege77  43902  frege93  43918  frege116  43941  frege118  43943  frege131  43956  frege133  43958  ntrneikb  44056  ismnuprim  44256  onfrALTlem5  44505  onfrALTlem5VD  44847  dfac5prim  44953  permaxpow  44972  permac8prim  44977  setis  49660