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  2348  sbnf2  2392  sb8mo  2631  raleqbii  3338  rmo5  3389  cbvrmo  3411  sstr2  3945  ss2ab  4016  sbcssg  4484  ssextss  5436  ssrel3  5774  relop  5838  dmcosseq  5970  dmcosseqOLD  5971  intasym  6117  intirr  6120  codir  6122  qfto  6123  cnvpo  6292  dfpo2  6301  dffun2  6550  dff14a  7273  porpss  7734  funcnvuni  7935  poxp  8130  infcllem  9455  ttrclss  9696  cp  9890  aceq2  10119  kmlem12  10161  kmlem15  10164  zfcndpow  10618  grothprim  10836  dfinfre  12213  infrenegsup  12215  xrinfmss2  13355  algcvgblem  16659  isprm2  16764  odulub  18485  oduglb  18487  isirred2  20551  isdomn3  20865  opprdomnb  20867  prmidl0  21530  ntreq0  23286  ist0-3  23554  ist1-3  23558  ordthaus  23593  dfconn2  23628  iscusp2  24511  mdsymlem8  32835  mo5f  32908  iuninc  32978  suppss2f  33056  tosglblem  33360  esumpfinvalf  34532  bnj110  35313  bnj92  35317  bnj539  35346  bnj540  35347  axrepprim  36233  axacprim  36238  dffr5  36285  dfso2  36286  elpotr  36310  mh-setind  37106  regsfromsetind  37109  bj-exexalal  37258  bj-cbvaew  37325  bj-alcomexcom  37362  bj-axseprep  37770  itg2addnclem2  38382  isdmn3  38785  sbcimi  38819  inxpss3  39029  trcoss2  39283  unitscyglem3  43024  eu6w  43468  moxfr  43483  ifpim123g  44286  elmapintrab  44362  undmrnresiss  44390  cnvssco  44392  snhesn  44572  psshepw  44574  frege77  44726  frege93  44742  frege116  44765  frege118  44767  frege131  44780  frege133  44782  ntrneikb  44880  ismnuprim  45064  onfrALTlem5  45311  onfrALTlem5VD  45653  dfac5prim  45759  permaxpow  45778  permac8prim  45783  isidom3  49169  setis  50535  alsbii  50637  ralsbii  50638  alseubii  50669  ralseubii  50670