Theorem imbi12i 352

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 348	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))
4	1, 2, 3	mp2 9	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  orimdi  941  nanbi  1520  rb-bijust  1769  sbnf  2345  sbnf2  2389  sb8mo  2628  raleqbii  3334  rmo5  3385  cbvrmo  3407  sstr2  3943  ss2ab  4014  sbcssg  4475  ssextss  5420  ssrel3  5758  relop  5822  dmcosseq  5954  dmcosseqOLD  5955  dmcosseqOLDOLD  5956  intasym  6102  intirr  6105  codir  6107  qfto  6108  cnvpo  6274  dfpo2  6283  dffun2  6531  dff14a  7254  porpss  7710  funcnvuni  7913  poxp  8108  infcllem  9434  ttrclss  9675  cp  9849  aceq2  10075  kmlem12  10118  kmlem15  10121  zfcndpow  10574  grothprim  10792  dfinfre  12173  infrenegsup  12175  xrinfmss2  13314  algcvgblem  16611  isprm2  16716  odulub  18437  oduglb  18439  isirred2  20470  isdomn2OLD  20762  isdomn3  20765  opprdomnb  20767  ntreq0  23137  ist0-3  23405  ist1-3  23409  ordthaus  23444  dfconn2  23479  iscusp2  24361  mdsymlem8  32613  mo5f  32688  iuninc  32760  suppss2f  32840  tosglblem  33152  prmidl0  33637  esumpfinvalf  34373  bnj110  35153  bnj92  35157  bnj539  35186  bnj540  35187  axrepprim  36052  axacprim  36057  dffr5  36104  dfso2  36105  elpotr  36129  mh-setind  36896  regsfromsetind  36899  bj-exexalal  37049  bj-cbvaew  37116  bj-alcomexcom  37153  bj-axseprep  37559  itg2addnclem2  38171  isdmn3  38573  sbcimi  38609  inxpss3  38819  trcoss2  39073  unitscyglem3  42814  eu6w  43258  moxfr  43273  ifpim123g  44076  elmapintrab  44152  undmrnresiss  44180  cnvssco  44182  snhesn  44362  psshepw  44364  frege77  44516  frege93  44532  frege116  44555  frege118  44557  frege131  44570  frege133  44572  ntrneikb  44670  ismnuprim  44870  onfrALTlem5  45118  onfrALTlem5VD  45460  dfac5prim  45566  permaxpow  45585  permac8prim  45590  setis  50319