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  1440  sbrim  1956  sbal1yz  2001  sbmo  2085  mo4f  2086  moanim  2100  necon4addc  2417  necon1bddc  2424  nfraldya  2512  r3al  2521  r19.23t  2584  ceqsralt  2764  ralab  2897  ralrab  2898  euind  2924  reu2  2925  rmo4  2930  rmo3f  2934  rmo4f  2935  reuind  2942  rmo3  3054  dfdif3  3245  raldifb  3275  unss  3309  ralunb  3316  inssdif0im  3490  ssundifim  3506  raaan  3529  pwss  3591  ralsnsg  3629  ralsns  3630  disjsn  3654  snssOLD  3718  snssb  3725  unissb  3839  intun  3875  intpr  3876  dfiin2g  3919  dftr2  4103  repizf2lem  4161  axpweq  4171  zfpow  4175  axpow2  4176  zfun  4434  uniex2  4436  setindel  4537  setind  4538  elirr  4540  en2lp  4553  zfregfr  4573  tfi  4581  raliunxp  4768  dffun2  5226  dffun4  5227  dffun4f  5232  dffun7  5243  funcnveq  5279  fununi  5284  pw1dc0el  6910  fiintim  6927  addnq0mo  7445  mulnq0mo  7446  addsrmo  7741  mulsrmo  7742  prime  9351  raluz2  9578  ralrp  9674  modfsummod  11465  nnwosdc  12039  isprm4  12118  dedekindicclemicc  14080  bdcriota  14605  bj-uniex2  14638  bj-ssom  14658