Theorem eqeq2 2362

Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem eqeq2

Step	Hyp	Ref	Expression
1		eqeq1 2359	. 2 |- (A = B -> (A = C <-> B = C))
2		eqcom 2355	. 2 |- (C = A <-> A = C)
3		eqcom 2355	. 2 |- (C = B <-> B = C)
4	1, 2, 3	3bitr4g 279	1 |- (A = B -> (C = A <-> C = B))

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  eqeq2i  2363  eqeq2d  2364  eqeq12  2365  eleq1  2413  neeq2  2526  alexeq  2969  ceqex  2970  pm13.183  2980  eqeu  3008  moeq3  3014  mo2icl  3016  mob2  3017  euind  3024  reu6i  3028  reuind  3040  sbc2or  3055  sbc5  3071  csbiebg  3176  eqif  3696  sneq  3745  preqr1  4125  preqr2g  4127  preq12bg  4129  opkelidkg  4275  iota5  4360  nndisjeq  4430  lefinlteq  4464  ltfintri  4467  evenodddisjlem1  4516  ideqg  4869  ideqg2  4870  fneq2  5175  foeq3  5268  fvelimab  5371  fvopab4t  5386  dff13f  5473  f1fveq  5474  opbr1st  5502  opbr2nd  5503  funsi  5521  ov3  5600  caovcan  5629  mpt2eq123  5662  ovmpt4g  5711  fnpprod  5844  fnfullfunlem1  5857  extd  5924  antid  5930  qsdisj  5996  ncspw1eu  6160  nchoicelem16  6305