Theorem eqeq1i 2240

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 2239	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  eqabb  2368  ssequn2  3392  ineqcom  3412  dfss1  3425  disj  3557  disjr  3558  undisj1  3566  undisj2  3567  uneqdifeqim  3595  reusn  3762  rabsneu  3764  eusn  3765  iin0r  4282  opeqsn  4369  unisuc  4534  onsucelsucexmid  4652  sucprcreg  4671  onintexmid  4695  dmopab3  4969  dm0rn0  4973  ssdmres  5060  imadisj  5124  args  5131  intirr  5149  dminxp  5207  dfrel3  5220  cbviotavw  5318  fntpg  5412  fncnv  5422  fresaunres1disj  5546  f0rn0  5562  dff1o4  5622  dffv4g  5667  fvun2  5744  fnreseql  5788  funopdmsn  5864  riota1  6023  riota2df  6025  riotaeqimp  6028  fnbrovb  6095  fnotovb  6096  ovid  6170  ov  6173  ovg  6193  f1od2  6431  frec0g  6628  diffitest  7144  ismkvnex  7446  prarloclem5  7815  renegcl  8534  elznn0  9592  seqf1oglem1  10881  seqf1oglem2  10882  hashunlem  11168  maxclpr  11907  gausslemma2d  15942  lgseisenlem1  15943  2lgslem4  15976  edg0iedg0g  16061  ushgredgedg  16221  ushgredgedgloop  16223  uhgr0v0e  16229  1loopgrvd2fi  16300  ex-ceil  16494  nninfsellemqall  16793  nninfomni  16797  iswomni0  16836