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  3378  dfss1  3409  disj  3541  disjr  3542  undisj1  3550  undisj2  3551  uneqdifeqim  3578  reusn  3740  rabsneu  3742  eusn  3743  iin0r  4257  opeqsn  4343  unisuc  4508  onsucelsucexmid  4626  sucprcreg  4645  onintexmid  4669  dmopab3  4942  dm0rn0  4946  ssdmres  5033  imadisj  5096  args  5103  intirr  5121  dminxp  5179  dfrel3  5192  cbviotavw  5290  fntpg  5383  fncnv  5393  f0rn0  5528  dff1o4  5588  dffv4g  5632  fvun2  5709  fnreseql  5753  funopdmsn  5829  riota1  5986  riota2df  5988  riotaeqimp  5991  fnbrovb  6058  fnotovb  6059  ovid  6133  ov  6136  ovg  6156  f1od2  6395  frec0g  6558  diffitest  7069  ismkvnex  7345  prarloclem5  7710  renegcl  8430  elznn0  9484  seqf1oglem1  10771  seqf1oglem2  10772  hashunlem  11057  maxclpr  11773  gausslemma2d  15788  lgseisenlem1  15789  2lgslem4  15822  edg0iedg0g  15907  ushgredgedg  16065  ushgredgedgloop  16067  uhgr0v0e  16073  1loopgrvd2fi  16111  ex-ceil  16258  nninfsellemqall  16553  nninfomni  16557  iswomni0  16591