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  1485  sbrim  2009  sbal1yz  2054  sbmo  2139  mo4f  2140  moanim  2154  necon4addc  2472  necon1bddc  2479  nfraldya  2567  r3al  2576  r19.23t  2640  ceqsralt  2830  ralab  2966  ralrab  2967  euind  2993  reu2  2994  rmo4  2999  rmo3f  3003  rmo4f  3004  reuind  3011  rmo3  3124  dfdif3  3317  raldifb  3347  unss  3381  ralunb  3388  inssdif0im  3562  ssundifim  3578  raaan  3600  pwss  3668  ralsnsg  3706  ralsns  3707  disjsn  3731  snssOLD  3799  snssb  3806  unissb  3923  intun  3959  intpr  3960  dfiin2g  4003  dftr2  4189  repizf2lem  4251  axpweq  4261  zfpow  4265  axpow2  4266  zfun  4531  uniex2  4533  setindel  4636  setind  4637  elirr  4639  en2lp  4652  zfregfr  4672  tfi  4680  raliunxp  4871  dffun2  5336  dffun4  5337  dffun4f  5342  dffun7  5353  funcnveq  5393  fununi  5398  pw1dc0el  7103  fiintim  7123  addnq0mo  7667  mulnq0mo  7668  addsrmo  7963  mulsrmo  7964  prime  9579  raluz2  9813  ralrp  9910  modfsummod  12037  nnwosdc  12628  isprm4  12709  dedekindicclemicc  15375  bdcriota  16529  bj-uniex2  16562  bj-ssom  16582