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  1459  sbrim  1983  sbal1yz  2028  sbmo  2112  mo4f  2113  moanim  2127  necon4addc  2445  necon1bddc  2452  nfraldya  2540  r3al  2549  r19.23t  2612  ceqsralt  2798  ralab  2932  ralrab  2933  euind  2959  reu2  2960  rmo4  2965  rmo3f  2969  rmo4f  2970  reuind  2977  rmo3  3089  dfdif3  3282  raldifb  3312  unss  3346  ralunb  3353  inssdif0im  3527  ssundifim  3543  raaan  3565  pwss  3631  ralsnsg  3669  ralsns  3670  disjsn  3694  snssOLD  3758  snssb  3765  unissb  3879  intun  3915  intpr  3916  dfiin2g  3959  dftr2  4143  repizf2lem  4204  axpweq  4214  zfpow  4218  axpow2  4219  zfun  4479  uniex2  4481  setindel  4584  setind  4585  elirr  4587  en2lp  4600  zfregfr  4620  tfi  4628  raliunxp  4817  dffun2  5278  dffun4  5279  dffun4f  5284  dffun7  5295  funcnveq  5331  fununi  5336  pw1dc0el  6990  fiintim  7010  addnq0mo  7542  mulnq0mo  7543  addsrmo  7838  mulsrmo  7839  prime  9454  raluz2  9682  ralrp  9779  modfsummod  11688  nnwosdc  12279  isprm4  12360  dedekindicclemicc  15022  bdcriota  15683  bj-uniex2  15716  bj-ssom  15736