Theorem eqeq1i 2237

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqeq1i	⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqeq1 2236	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  ssequn2  3377  dfss1  3408  disj  3540  disjr  3541  undisj1  3549  undisj2  3550  uneqdifeqim  3577  reusn  3737  rabsneu  3739  eusn  3740  iin0r  4252  opeqsn  4338  unisuc  4503  onsucelsucexmid  4621  sucprcreg  4640  onintexmid  4664  dmopab3  4935  dm0rn0  4939  ssdmres  5026  imadisj  5089  args  5096  intirr  5114  dminxp  5172  dfrel3  5185  cbviotavw  5283  fntpg  5376  fncnv  5386  f0rn0  5519  dff1o4  5579  dffv4g  5623  fvun2  5700  fnreseql  5744  funopdmsn  5818  riota1  5973  riota2df  5975  riotaeqimp  5978  fnbrovb  6045  fnotovb  6046  ovid  6120  ov  6123  ovg  6143  f1od2  6379  frec0g  6541  diffitest  7045  ismkvnex  7318  prarloclem5  7683  renegcl  8403  elznn0  9457  seqf1oglem1  10736  seqf1oglem2  10737  hashunlem  11021  maxclpr  11728  gausslemma2d  15742  lgseisenlem1  15743  2lgslem4  15776  edg0iedg0g  15860  ushgredgedg  16018  ushgredgedgloop  16020  ex-ceil  16048  nninfsellemqall  16340  nninfomni  16344  iswomni0  16378