Theorem eqeq1i 2242

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

Hypothesis

Ref	Expression
eqeq1i.1	|- A = B

Assertion

Ref	Expression
eqeq1i	|- ( A = C <-> B = C )

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 |- A = B
2		eqeq1 2241	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	ax-mp 5	1 |- ( A = C <-> B = C )

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 2216

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

This theorem is referenced by:  eqabb  2370  ssequn2  3396  ineqcom  3416  dfss1  3429  disj  3561  disjr  3562  undisj1  3570  undisj2  3571  uneqdifeqim  3599  reusn  3767  rabsneu  3769  eusn  3770  iin0r  4287  opeqsn  4374  unisuc  4539  onsucelsucexmid  4657  sucprcreg  4676  onintexmid  4700  dmopab3  4974  dm0rn0  4978  ssdmres  5065  imadisj  5129  args  5136  intirr  5154  dminxp  5212  dfrel3  5225  cbviotavw  5323  fntpg  5417  fncnv  5427  fresaunres1disj  5551  f0rn0  5567  dff1o4  5627  dffv4g  5672  fvun2  5749  fnreseql  5793  funopdmsn  5869  riota1  6031  riota2df  6033  riotaeqimp  6036  fnbrovb  6103  fnotovb  6104  ovid  6178  ov  6181  ovg  6201  f1od2  6444  frec0g  6641  diffitest  7157  ismkvnex  7459  prarloclem5  7831  renegcl  8550  addeq0  8666  elznn0  9609  seqf1oglem1  10905  seqf1oglem2  10906  hashunlem  11193  maxclpr  11932  gausslemma2d  16068  lgseisenlem1  16069  2lgslem4  16102  edg0iedg0g  16187  ushgredgedg  16347  ushgredgedgloop  16349  uhgr0v0e  16355  1loopgrvd2fi  16426  ex-ceil  16620  nninfsellemqall  16919  nninfomni  16923  iswomni0  16962