Theorem imbi12i 353

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  orimdi  944  nanbi  1530  rb-bijust  1782  sbnf  2344  sbnf2  2387  sb8mo  2626  raleqbii  3332  rmo5  3383  cbvrmo  3405  sstr2  3938  ss2ab  4009  sbcssg  4477  ssextss  5428  ssrel3  5766  relop  5830  dmcosseq  5962  dmcosseqOLD  5963  intasym  6109  intirr  6112  codir  6114  qfto  6115  cnvpo  6285  dfpo2  6294  dffun2  6543  dff14a  7268  porpss  7729  funcnvuni  7930  poxp  8127  infcllem  9459  ttrclss  9700  cp  9894  aceq2  10123  kmlem12  10165  kmlem15  10168  zfcndpow  10626  grothprim  10844  dfinfre  12221  infrenegsup  12223  xrinfmss2  13364  algcvgblem  16668  isprm2  16773  odulub  18494  oduglb  18496  isirred2  20563  isdomn3  20877  opprdomnb  20879  prmidl0  21542  ntreq0  23303  ist0-3  23571  ist1-3  23575  ordthaus  23610  dfconn2  23645  iscusp2  24528  mdsymlem8  32892  mo5f  32965  iuninc  33035  suppss2f  33112  tosglblem  33415  esumpfinvalf  34587  bnj110  35368  bnj92  35372  bnj539  35401  bnj540  35402  axrepprim  36282  axacprim  36287  dfso2  36335  elpotr  36359  mh-setind  37156  regsfromsetind  37159  bj-exexalal  37308  bj-cbvaew  37375  bj-alcomexcom  37412  bj-axseprep  37820  itg2addnclem2  38422  isdmn3  38825  sbcimi  38859  inxpss3  39069  trcoss2  39323  unitscyglem3  43064  eu6w  43523  moxfr  43538  ifpim123g  44341  elmapintrab  44417  undmrnresiss  44445  cnvssco  44447  snhesn  44627  psshepw  44629  frege77  44781  frege93  44797  frege116  44820  frege118  44822  frege131  44835  frege133  44837  ntrneikb  44935  ismnuprim  45119  onfrALTlem5  45366  onfrALTlem5VD  45708  dfac5prim  45814  permaxpow  45833  permac8prim  45838  isidom3  49261  setis  50625  alsbii  50730  ralsbii  50731  alseubii  50762  ralseubii  50763