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  2827  ralab  2963  ralrab  2964  euind  2990  reu2  2991  rmo4  2996  rmo3f  3000  rmo4f  3001  reuind  3008  rmo3  3121  dfdif3  3314  raldifb  3344  unss  3378  ralunb  3385  inssdif0im  3559  ssundifim  3575  raaan  3597  pwss  3665  ralsnsg  3703  ralsns  3704  disjsn  3728  snssOLD  3793  snssb  3800  unissb  3917  intun  3953  intpr  3954  dfiin2g  3997  dftr2  4183  repizf2lem  4244  axpweq  4254  zfpow  4258  axpow2  4259  zfun  4524  uniex2  4526  setindel  4629  setind  4630  elirr  4632  en2lp  4645  zfregfr  4665  tfi  4673  raliunxp  4862  dffun2  5327  dffun4  5328  dffun4f  5333  dffun7  5344  funcnveq  5383  fununi  5388  pw1dc0el  7069  fiintim  7089  addnq0mo  7630  mulnq0mo  7631  addsrmo  7926  mulsrmo  7927  prime  9542  raluz2  9770  ralrp  9867  modfsummod  11964  nnwosdc  12555  isprm4  12636  dedekindicclemicc  15300  bdcriota  16204  bj-uniex2  16237  bj-ssom  16257