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 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  imbi12i  239  ancomsimp  1490  sbrim  2016  sbal1yz  2061  sbmo  2146  mo4f  2147  moanim  2161  necon4addc  2490  necon1bddc  2497  nfraldya  2585  r3al  2594  r19.23t  2658  ceqsralt  2849  ralab  2986  ralrab  2987  euind  3013  reu2  3014  rmo4  3019  rmo3f  3023  rmo4f  3024  reuind  3031  rmo3  3144  dfdif3  3339  raldifb  3369  unss  3403  ralunb  3410  inssdif0imOLD  3593  ssundifim  3611  raaan  3633  pwss  3708  ralsnsg  3746  ralsns  3747  disjsn  3771  snssOLD  3840  snssb  3848  unissb  3965  intun  4001  intpr  4002  dfiin2g  4045  dftr2  4231  repizf2lem  4298  axpweq  4308  zfpow  4312  axpow2  4313  zfun  4579  uniex2OLD  4582  setindel  4685  setind  4686  elirr  4688  en2lp  4701  zfregfr  4721  tfi  4729  raliunxp  4921  dffun2  5387  dffun4  5388  dffun4f  5393  dffun7  5404  funcnveq  5444  fununi  5449  pw1dc0el  7218  fiintim  7238  addnq0mo  7814  mulnq0mo  7815  addsrmo  8110  mulsrmo  8111  prime  9745  raluz2  9979  ralrp  10076  modfsummod  12225  nnwosdc  12816  isprm4  12897  dedekindicclemicc  15733  bdcriota  16909  bj-ssom  16962  exmidpeirce  17038