Theorem eqeq1i 2122

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 2121	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	ax-mp 7	1 |- ( A = C <-> B = C )

Syntax hints:   <-> wb 104   = wceq 1314

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-cleq 2108

This theorem is referenced by:  ssequn2  3215  dfss1  3246  disj  3377  disjr  3378  undisj1  3386  undisj2  3387  uneqdifeqim  3414  reusn  3560  rabsneu  3562  eusn  3563  iin0r  4053  opeqsn  4134  unisuc  4295  onsucelsucexmid  4405  sucprcreg  4424  onintexmid  4447  dmopab3  4712  dm0rn0  4716  ssdmres  4799  imadisj  4859  args  4866  intirr  4883  dminxp  4941  dfrel3  4954  fntpg  5137  fncnv  5147  f0rn0  5275  dff1o4  5331  dffv4g  5372  fvun2  5442  fnreseql  5484  riota1  5702  riota2df  5704  fnotovb  5768  ovid  5841  ov  5844  ovg  5863  f1od2  6086  frec0g  6248  diffitest  6734  ismkvnex  6979  prarloclem5  7256  renegcl  7946  elznn0  8973  hashunlem  10443  maxclpr  10886  ex-ceil  12631  nninfsellemqall  12903  nninfomni  12907