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  2525  alexeq  2968  ceqex  2969  pm13.183  2979  eqeu  3007  moeq3  3013  mo2icl  3015  mob2  3016  euind  3023  reu6i  3027  reuind  3039  sbc2or  3054  sbc5  3070  csbiebg  3175  eqif  3695  sneq  3744  preqr1  4124  preqr2g  4126  preq12bg  4128  opkelidkg  4274  iota5  4359  nndisjeq  4429  lefinlteq  4463  ltfintri  4466  evenodddisjlem1  4515  ideqg  4868  ideqg2  4869  fneq2  5174  foeq3  5267  fvelimab  5370  fvopab4t  5385  dff13f  5472  f1fveq  5473  opbr1st  5501  opbr2nd  5502  funsi  5520  ov3  5599  caovcan  5628  mpt2eq123  5661  ovmpt4g  5710  fnpprod  5843  fnfullfunlem1  5856  extd  5923  antid  5929  qsdisj  5995  ncspw1eu  6159  nchoicelem16  6304