Theorem imbi12i 349

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 345	. 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  1496  rb-bijust  1749  sbnf2  2352  sb8mo  2593  cbvmowOLD  2596  raleqbii  3336  sbralie  3352  rmo5  3394  cbvrmowOLD  3409  cbvrmo  3423  ss2ab  4055  sbcssg  4522  ssextss  5452  ssrel3  5785  relop  5849  dmcosseq  5971  cotrgOLDOLD  6109  cnvsymOLDOLD  6114  intasym  6115  intirr  6118  codir  6120  qfto  6121  cnvpo  6285  dfpo2  6294  dffun2  6552  dffun2OLD  6553  dff14a  7271  porpss  7719  funcnvuni  7924  poxp  8116  infcllem  9484  ttrclss  9717  cp  9888  aceq2  10116  kmlem12  10158  kmlem15  10161  zfcndpow  10613  grothprim  10831  dfinfre  12199  infrenegsup  12201  xrinfmss2  13294  algcvgblem  16518  isprm2  16623  odulub  18364  oduglb  18366  isirred2  20312  isdomn2  21115  ntreq0  22801  ist0-3  23069  ist1-3  23073  ordthaus  23108  dfconn2  23143  iscusp2  24027  mdsymlem8  31930  mo5f  31996  iuninc  32059  suppss2f  32130  tosglblem  32411  prmidl0  32843  esumpfinvalf  33372  bnj110  34167  bnj92  34171  bnj539  34200  bnj540  34201  axrepprim  34975  axacprim  34980  dffr5  35028  dfso2  35029  elpotr  35057  bj-alcomexcom  35861  itg2addnclem2  36843  isdmn3  37245  sbcimi  37281  inxpss3  37486  trcoss2  37657  moxfr  41732  isdomn3  42248  ifpim123g  42553  elmapintrab  42629  undmrnresiss  42657  cnvssco  42659  snhesn  42839  psshepw  42841  frege77  42993  frege93  43009  frege116  43032  frege118  43034  frege131  43047  frege133  43049  ntrneikb  43147  ismnuprim  43355  onfrALTlem5  43605  onfrALTlem5VD  43948  setis  47830