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  1483  sbrim  2007  sbal1yz  2052  sbmo  2137  mo4f  2138  moanim  2152  necon4addc  2470  necon1bddc  2477  nfraldya  2565  r3al  2574  r19.23t  2638  ceqsralt  2828  ralab  2964  ralrab  2965  euind  2991  reu2  2992  rmo4  2997  rmo3f  3001  rmo4f  3002  reuind  3009  rmo3  3122  dfdif3  3315  raldifb  3345  unss  3379  ralunb  3386  inssdif0im  3560  ssundifim  3576  raaan  3598  pwss  3666  ralsnsg  3704  ralsns  3705  disjsn  3729  snssOLD  3797  snssb  3804  unissb  3921  intun  3957  intpr  3958  dfiin2g  4001  dftr2  4187  repizf2lem  4249  axpweq  4259  zfpow  4263  axpow2  4264  zfun  4529  uniex2  4531  setindel  4634  setind  4635  elirr  4637  en2lp  4650  zfregfr  4670  tfi  4678  raliunxp  4869  dffun2  5334  dffun4  5335  dffun4f  5340  dffun7  5351  funcnveq  5390  fununi  5395  pw1dc0el  7096  fiintim  7116  addnq0mo  7657  mulnq0mo  7658  addsrmo  7953  mulsrmo  7954  prime  9569  raluz2  9803  ralrp  9900  modfsummod  12009  nnwosdc  12600  isprm4  12681  dedekindicclemicc  15346  bdcriota  16414  bj-uniex2  16447  bj-ssom  16467