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 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  orimdi  943  nanbi  1530  rb-bijust  1779  sbnf  2346  sbnf2  2390  sb8mo  2629  raleqbii  3336  rmo5  3387  cbvrmo  3409  sstr2  3944  ss2ab  4015  sbcssg  4482  ssextss  5434  ssrel3  5772  relop  5836  dmcosseq  5968  dmcosseqOLD  5969  intasym  6115  intirr  6118  codir  6120  qfto  6121  cnvpo  6288  dfpo2  6297  dffun2  6546  dff14a  7268  porpss  7724  funcnvuni  7925  poxp  8120  infcllem  9444  ttrclss  9685  cp  9873  aceq2  10099  kmlem12  10141  kmlem15  10144  zfcndpow  10596  grothprim  10814  dfinfre  12191  infrenegsup  12193  xrinfmss2  13332  algcvgblem  16630  isprm2  16735  odulub  18456  oduglb  18458  isirred2  20499  isdomn3  20813  opprdomnb  20815  prmidl0  21478  ntreq0  23234  ist0-3  23502  ist1-3  23506  ordthaus  23541  dfconn2  23576  iscusp2  24458  mdsymlem8  32762  mo5f  32835  iuninc  32905  suppss2f  32983  tosglblem  33294  esumpfinvalf  34466  bnj110  35246  bnj92  35250  bnj539  35279  bnj540  35280  axrepprim  36194  axacprim  36199  dffr5  36246  dfso2  36247  elpotr  36271  mh-setind  37067  regsfromsetind  37070  bj-exexalal  37219  bj-cbvaew  37286  bj-alcomexcom  37323  bj-axseprep  37731  itg2addnclem2  38343  isdmn3  38745  sbcimi  38779  inxpss3  38989  trcoss2  39243  unitscyglem3  42984  eu6w  43428  moxfr  43443  ifpim123g  44246  elmapintrab  44322  undmrnresiss  44350  cnvssco  44352  snhesn  44532  psshepw  44534  frege77  44686  frege93  44702  frege116  44725  frege118  44727  frege131  44740  frege133  44742  ntrneikb  44840  ismnuprim  45024  onfrALTlem5  45271  onfrALTlem5VD  45613  dfac5prim  45719  permaxpow  45738  permac8prim  45743  isidom3  49130  setis  50496  alsbii  50598  ralsbii  50599  alseubii  50630  ralseubii  50631