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 205

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 206

This theorem is referenced by:  orimdi  927  nanbi  1492  rb-bijust  1753  sbnf2  2356  sb8mo  2601  cbvmowOLD  2604  raleqbii  3160  rmo5  3355  cbvrmowOLD  3367  cbvrmo  3371  ss2ab  3989  sbcssg  4451  ssextss  5363  relop  5748  dmcosseq  5871  cotrg  6005  cnvsym  6008  intasym  6009  intirr  6012  codir  6014  qfto  6015  cnvpo  6179  dfpo2  6188  dff14a  7124  porpss  7558  funcnvuni  7752  poxp  7940  infcllem  9176  cp  9580  aceq2  9806  kmlem12  9848  kmlem15  9851  zfcndpow  10303  grothprim  10521  dfinfre  11886  infrenegsup  11888  xrinfmss2  12974  algcvgblem  16210  isprm2  16315  odulub  18040  oduglb  18042  isirred2  19858  isdomn2  20483  ntreq0  22136  ist0-3  22404  ist1-3  22408  ordthaus  22443  dfconn2  22478  iscusp2  23362  mdsymlem8  30673  mo5f  30738  iuninc  30801  suppss2f  30875  tosglblem  31154  prmidl0  31528  esumpfinvalf  31944  bnj110  32738  bnj92  32742  bnj539  32771  bnj540  32772  axrepprim  33543  axacprim  33548  dffr5  33627  dfso2  33628  elpotr  33663  ttrclss  33706  bj-alcomexcom  34789  itg2addnclem2  35756  isdmn3  36159  sbcimi  36195  ssrel3  36361  inxpss3  36376  trcoss2  36529  moxfr  40430  isdomn3  40945  ifpim123g  41005  elmapintrab  41073  undmrnresiss  41101  cnvssco  41103  snhesn  41283  psshepw  41285  frege77  41437  frege93  41453  frege116  41476  frege118  41478  frege131  41491  frege133  41493  ntrneikb  41593  ismnuprim  41801  onfrALTlem5  42051  onfrALTlem5VD  42394  setis  46289