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  1496  rb-bijust  1745  sbnf  2310  sbnf2  2358  sb8mo  2598  raleqbii  3341  rmo5  3397  cbvrmo  3425  sstr2  4001  ss2ab  4071  sbcssg  4525  ssextss  5463  ssrel3  5798  relop  5863  dmcosseq  5989  dmcosseqOLD  5990  cotrgOLDOLD  6131  cnvsymOLDOLD  6136  intasym  6137  intirr  6140  codir  6142  qfto  6143  cnvpo  6308  dfpo2  6317  dffun2  6572  dffun2OLD  6573  dff14a  7289  porpss  7745  funcnvuni  7954  poxp  8151  infcllem  9524  ttrclss  9757  cp  9928  aceq2  10156  kmlem12  10199  kmlem15  10202  zfcndpow  10653  grothprim  10871  dfinfre  12246  infrenegsup  12248  xrinfmss2  13349  algcvgblem  16610  isprm2  16715  odulub  18464  oduglb  18466  isirred2  20437  isdomn2OLD  20728  isdomn3  20731  opprdomnb  20733  ntreq0  23100  ist0-3  23368  ist1-3  23372  ordthaus  23407  dfconn2  23442  iscusp2  24326  mdsymlem8  32438  mo5f  32516  iuninc  32580  suppss2f  32654  tosglblem  32948  prmidl0  33457  esumpfinvalf  34056  bnj110  34850  bnj92  34854  bnj539  34883  bnj540  34884  axrepprim  35681  axacprim  35686  dffr5  35733  dfso2  35734  elpotr  35762  bj-alcomexcom  36662  itg2addnclem2  37658  isdmn3  38060  sbcimi  38096  inxpss3  38295  trcoss2  38465  unitscyglem3  42178  eu6w  42662  moxfr  42679  ifpim123g  43489  elmapintrab  43565  undmrnresiss  43593  cnvssco  43595  snhesn  43775  psshepw  43777  frege77  43929  frege93  43945  frege116  43968  frege118  43970  frege131  43983  frege133  43985  ntrneikb  44083  ismnuprim  44289  onfrALTlem5  44539  onfrALTlem5VD  44882  setis  48928