Theorem imbi1i 237

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 235	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
3	1, 2	ax-mp 5	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imbi12i  238  ancomsimp  1420  sbrim  1936  sbal1yz  1981  sbmo  2065  mo4f  2066  moanim  2080  necon4addc  2397  necon1bddc  2404  nfraldya  2492  r3al  2501  r19.23t  2564  ceqsralt  2739  ralab  2872  ralrab  2873  euind  2899  reu2  2900  rmo4  2905  rmo3f  2909  rmo4f  2910  reuind  2917  rmo3  3028  dfdif3  3217  raldifb  3247  unss  3281  ralunb  3288  inssdif0im  3461  ssundifim  3477  raaan  3500  pwss  3559  ralsnsg  3596  ralsns  3597  disjsn  3621  snss  3685  unissb  3802  intun  3838  intpr  3839  dfiin2g  3882  dftr2  4064  repizf2lem  4122  axpweq  4132  zfpow  4136  axpow2  4137  zfun  4394  uniex2  4396  setindel  4497  setind  4498  elirr  4500  en2lp  4513  zfregfr  4533  tfi  4541  raliunxp  4727  dffun2  5180  dffun4  5181  dffun4f  5186  dffun7  5197  funcnveq  5233  fununi  5238  pw1dc0el  6856  fiintim  6873  addnq0mo  7367  mulnq0mo  7368  addsrmo  7663  mulsrmo  7664  prime  9263  raluz2  9490  ralrp  9582  modfsummod  11355  isprm4  11995  dedekindicclemicc  13010  bdcriota  13458  bj-uniex2  13491  bj-ssom  13511