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  3307  rmo5  3363  cbvrmo  3387  sstr2  3942  ss2ab  4014  sbcssg  4471  ssextss  5396  ssrel3  5729  relop  5793  dmcosseq  5919  dmcosseqOLD  5920  dmcosseqOLDOLD  5921  intasym  6064  intirr  6067  codir  6069  qfto  6070  cnvpo  6235  dfpo2  6244  dffun2  6492  dff14a  7207  porpss  7663  funcnvuni  7865  poxp  8061  infcllem  9378  ttrclss  9616  cp  9787  aceq2  10013  kmlem12  10056  kmlem15  10059  zfcndpow  10510  grothprim  10728  dfinfre  12106  infrenegsup  12108  xrinfmss2  13213  algcvgblem  16488  isprm2  16593  odulub  18311  oduglb  18313  isirred2  20306  isdomn2OLD  20597  isdomn3  20600  opprdomnb  20602  ntreq0  22962  ist0-3  23230  ist1-3  23234  ordthaus  23269  dfconn2  23304  iscusp2  24187  mdsymlem8  32354  mo5f  32433  iuninc  32504  suppss2f  32581  tosglblem  32916  prmidl0  33387  esumpfinvalf  34043  bnj110  34825  bnj92  34829  bnj539  34858  bnj540  34859  axrepprim  35679  axacprim  35684  dffr5  35731  dfso2  35732  elpotr  35759  bj-alcomexcom  36658  itg2addnclem2  37656  isdmn3  38058  sbcimi  38094  inxpss3  38292  trcoss2  38465  unitscyglem3  42174  eu6w  42653  moxfr  42669  ifpim123g  43477  elmapintrab  43553  undmrnresiss  43581  cnvssco  43583  snhesn  43763  psshepw  43765  frege77  43917  frege93  43933  frege116  43956  frege118  43958  frege131  43971  frege133  43973  ntrneikb  44071  ismnuprim  44271  onfrALTlem5  44520  onfrALTlem5VD  44862  dfac5prim  44968  permaxpow  44987  permac8prim  44992  setis  49687