Theorem imbi1i 238

Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis

Ref	Expression
imbi1i.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
imbi1i	⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Proof of Theorem imbi1i

Step	Hyp	Ref	Expression
1		imbi1i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		imbi1 236	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
3	1, 2	ax-mp 5	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imbi12i  239  ancomsimp  1461  sbrim  1985  sbal1yz  2030  sbmo  2114  mo4f  2115  moanim  2129  necon4addc  2447  necon1bddc  2454  nfraldya  2542  r3al  2551  r19.23t  2614  ceqsralt  2801  ralab  2937  ralrab  2938  euind  2964  reu2  2965  rmo4  2970  rmo3f  2974  rmo4f  2975  reuind  2982  rmo3  3094  dfdif3  3287  raldifb  3317  unss  3351  ralunb  3358  inssdif0im  3532  ssundifim  3548  raaan  3570  pwss  3637  ralsnsg  3675  ralsns  3676  disjsn  3700  snssOLD  3765  snssb  3772  unissb  3886  intun  3922  intpr  3923  dfiin2g  3966  dftr2  4152  repizf2lem  4213  axpweq  4223  zfpow  4227  axpow2  4228  zfun  4489  uniex2  4491  setindel  4594  setind  4595  elirr  4597  en2lp  4610  zfregfr  4630  tfi  4638  raliunxp  4827  dffun2  5290  dffun4  5291  dffun4f  5296  dffun7  5307  funcnveq  5346  fununi  5351  pw1dc0el  7023  fiintim  7043  addnq0mo  7580  mulnq0mo  7581  addsrmo  7876  mulsrmo  7877  prime  9492  raluz2  9720  ralrp  9817  modfsummod  11844  nnwosdc  12435  isprm4  12516  dedekindicclemicc  15179  bdcriota  15957  bj-uniex2  15990  bj-ssom  16010