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  1459  sbrim  1983  sbal1yz  2028  sbmo  2112  mo4f  2113  moanim  2127  necon4addc  2445  necon1bddc  2452  nfraldya  2540  r3al  2549  r19.23t  2612  ceqsralt  2798  ralab  2932  ralrab  2933  euind  2959  reu2  2960  rmo4  2965  rmo3f  2969  rmo4f  2970  reuind  2977  rmo3  3089  dfdif3  3282  raldifb  3312  unss  3346  ralunb  3353  inssdif0im  3527  ssundifim  3543  raaan  3565  pwss  3631  ralsnsg  3669  ralsns  3670  disjsn  3694  snssOLD  3758  snssb  3765  unissb  3879  intun  3915  intpr  3916  dfiin2g  3959  dftr2  4143  repizf2lem  4204  axpweq  4214  zfpow  4218  axpow2  4219  zfun  4480  uniex2  4482  setindel  4585  setind  4586  elirr  4588  en2lp  4601  zfregfr  4621  tfi  4629  raliunxp  4818  dffun2  5280  dffun4  5281  dffun4f  5286  dffun7  5297  funcnveq  5336  fununi  5341  pw1dc0el  7007  fiintim  7027  addnq0mo  7559  mulnq0mo  7560  addsrmo  7855  mulsrmo  7856  prime  9471  raluz2  9699  ralrp  9796  modfsummod  11711  nnwosdc  12302  isprm4  12383  dedekindicclemicc  15046  bdcriota  15752  bj-uniex2  15785  bj-ssom  15805