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  4233  repizf2lem  4300  axpweq  4310  zfpow  4314  axpow2  4315  zfun  4581  uniex2OLD  4584  setindel  4687  setind  4688  elirr  4690  en2lp  4703  zfregfr  4723  tfi  4731  raliunxp  4923  dffun2  5390  dffun4  5391  dffun4f  5396  dffun7  5407  funcnveq  5447  fununi  5452  pw1dc0el  7222  fiintim  7242  addnq0mo  7820  mulnq0mo  7821  addsrmo  8116  mulsrmo  8117  prime  9756  raluz2  9995  ralrp  10093  modfsummod  12250  nnwosdc  12841  isprm4  12922  dedekindicclemicc  15858  bdcriota  17114  bj-ssom  17167  exmidpeirce  17243