Theorem imbi12i 339

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  orimdi  910  nanbi  1494  rb-bijust  1714  nfbiiOLD  1876  sbnf2  2467  sb8mo  2533  cbvmo  2535  raleqbii  3019  rmo5  3192  cbvrmo  3200  ss2ab  3703  sbcssg  4118  trint  4801  ssextss  4952  relop  5305  dmcosseq  5419  cotrg  5542  issref  5544  cnvsym  5545  intasym  5546  intirr  5549  codir  5551  qfto  5552  cnvpo  5711  dff14a  6567  porpss  6983  funcnvuni  7161  poxp  7334  infcllem  8434  cp  8792  aceq2  8980  kmlem12  9021  kmlem15  9024  zfcndpow  9476  grothprim  9694  dfinfre  11042  infrenegsup  11044  xrinfmss2  12179  algcvgblem  15337  isprm2  15442  oduglb  17186  odulub  17188  isirred2  18747  isdomn2  19347  ntreq0  20929  ist0-3  21197  ist1-3  21201  ordthaus  21236  dfconn2  21270  iscusp2  22153  mdsymlem8  29397  mo5f  29452  iuninc  29505  suppss2f  29567  tosglblem  29797  esumpfinvalf  30266  bnj110  31054  bnj92  31058  bnj539  31087  bnj540  31088  axrepprim  31705  axacprim  31710  dffr5  31769  dfso2  31770  dfpo2  31771  elpotr  31810  gtinfOLD  32439  bj-alcomexcom  32795  itg2addnclem2  33592  isdmn3  34003  sbcimi  34042  ssrel3  34208  inxpss3  34225  trcoss2  34374  moxfr  37572  isdomn3  38099  ifpim123g  38162  elmapintrab  38199  undmrnresiss  38227  cnvssco  38229  snhesn  38397  psshepw  38399  frege77  38551  frege93  38567  frege116  38590  frege118  38592  frege131  38605  frege133  38607  ntrneikb  38709  conss34OLD  38963  onfrALTlem5  39074  onfrALTlem5VD  39435  setis  42769