Theorem imbi12i 343

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  orimdi  914  nanbi  1475  rb-bijust  1712  sbnf2  2291  sb8mo  2635  cbvmoOLD  2639  raleqbii  3175  rmo5  3368  cbvrmo  3376  ss2ab  3923  sbcssg  4340  trintOLD  5043  ssextss  5199  relop  5567  dmcosseq  5683  cotrg  5808  cnvsym  5811  intasym  5812  intirr  5815  codir  5817  qfto  5818  cnvpo  5973  dff14a  6851  porpss  7269  funcnvuni  7449  poxp  7625  infcllem  8744  cp  9112  aceq2  9337  kmlem12  9379  kmlem15  9382  zfcndpow  9834  grothprim  10052  dfinfre  11421  infrenegsup  11423  xrinfmss2  12518  algcvgblem  15775  isprm2  15880  oduglb  17619  odulub  17621  isirred2  19186  isdomn2  19805  ntreq0  21401  ist0-3  21669  ist1-3  21673  ordthaus  21708  dfconn2  21743  iscusp2  22626  mdsymlem8  29980  mo5f  30047  iuninc  30095  suppss2f  30160  tosglblem  30411  esumpfinvalf  31008  bnj110  31806  bnj92  31810  bnj539  31839  bnj540  31840  axrepprim  32477  axacprim  32482  dffr5  32538  dfso2  32539  dfpo2  32540  elpotr  32575  bj-alcomexcom  33553  itg2addnclem2  34414  isdmn3  34823  sbcimi  34861  ssrel3  35029  inxpss3  35044  trcoss2  35198  moxfr  38713  isdomn3  39229  ifpim123g  39291  elmapintrab  39327  undmrnresiss  39355  cnvssco  39357  snhesn  39524  psshepw  39526  frege77  39678  frege93  39694  frege116  39717  frege118  39719  frege131  39732  frege133  39734  ntrneikb  39836  ismnuprim  40034  onfrALTlem5  40324  onfrALTlem5VD  40667  setis  44192