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 195

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 196

This theorem is referenced by:  orimdi  888  nanbi  1446  rb-bijust  1665  nfbii  1770  nfbiiOLD  1824  sbnf2  2427  sb8mo  2492  cbvmo  2494  raleqbii  2973  rmo5  3139  cbvrmo  3146  ss2ab  3633  sbcssg  4035  trint  4696  ssextss  4849  relop  5194  dmcosseq  5308  cotrg  5426  issref  5428  cnvsym  5429  intasym  5430  intirr  5433  codir  5435  qfto  5436  cnvpo  5590  dff14a  6427  porpss  6839  funcnvuni  7012  poxp  7176  infcllem  8276  cp  8637  aceq2  8825  kmlem12  8866  kmlem15  8869  zfcndpow  9317  grothprim  9535  dfinfre  10881  infrenegsup  10883  xrinfmss2  12013  algcvgblem  15128  isprm2  15233  oduglb  16962  odulub  16964  isirred2  18524  isdomn2  19120  ntreq0  20691  ist0-3  20959  ist1-3  20963  ordthaus  20998  dfcon2  21032  iscusp2  21916  mdsymlem8  28653  mo5f  28708  iuninc  28761  suppss2f  28819  tosglblem  29000  esumpfinvalf  29465  bnj110  30182  bnj92  30186  bnj539  30215  bnj540  30216  axrepprim  30833  axacprim  30838  dffr5  30896  dfso2  30897  dfpo2  30898  elpotr  30930  gtinfOLD  31484  bj-alcomexcom  31857  itg2addnclem2  32632  isdmn3  33043  sbcimi  33082  moxfr  36273  isdomn3  36801  ifpim123g  36864  elmapintrab  36901  undmrnresiss  36929  cnvssco  36931  snhesn  37100  psshepw  37102  frege77  37254  frege93  37270  frege116  37293  frege118  37295  frege131  37308  frege133  37310  ntrneikb  37412  conss34OLD  37667  onfrALTlem5  37778  onfrALTlem5VD  38143  frgr2wwlkeqm  41496