Theorem imbi12i 340

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 336	. 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  892  nanbi  1454  rb-bijust  1674  nfbiiOLD  1836  sbnf2  2439  sb8mo  2504  cbvmo  2506  raleqbii  2990  rmo5  3162  cbvrmo  3170  ss2ab  3670  sbcssg  4085  trint  4768  ssextss  4922  relop  5272  dmcosseq  5387  cotrg  5507  issref  5509  cnvsym  5510  intasym  5511  intirr  5514  codir  5516  qfto  5517  cnvpo  5673  dff14a  6527  porpss  6941  funcnvuni  7119  poxp  7289  infcllem  8393  cp  8754  aceq2  8942  kmlem12  8983  kmlem15  8986  zfcndpow  9438  grothprim  9656  dfinfre  11004  infrenegsup  11006  xrinfmss2  12141  algcvgblem  15290  isprm2  15395  oduglb  17139  odulub  17141  isirred2  18701  isdomn2  19299  ntreq0  20881  ist0-3  21149  ist1-3  21153  ordthaus  21188  dfconn2  21222  iscusp2  22106  mdsymlem8  29269  mo5f  29324  iuninc  29379  suppss2f  29439  tosglblem  29669  esumpfinvalf  30138  bnj110  30928  bnj92  30932  bnj539  30961  bnj540  30962  axrepprim  31579  axacprim  31584  dffr5  31643  dfso2  31644  dfpo2  31645  elpotr  31686  gtinfOLD  32314  bj-alcomexcom  32670  itg2addnclem2  33462  isdmn3  33873  sbcimi  33912  ssrel3  34067  inxpss3  34084  moxfr  37255  isdomn3  37782  ifpim123g  37845  elmapintrab  37882  undmrnresiss  37910  cnvssco  37912  snhesn  38080  psshepw  38082  frege77  38234  frege93  38250  frege116  38273  frege118  38275  frege131  38288  frege133  38290  ntrneikb  38392  conss34OLD  38646  onfrALTlem5  38757  onfrALTlem5VD  39121