Theorem eqeq2 2206

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 2203	. 2 |- ( A = B -> ( A = C <-> B = C ) )
2		eqcom 2198	. 2 |- ( C = A <-> A = C )
3		eqcom 2198	. 2 |- ( C = B <-> B = C )
4	1, 2, 3	3bitr4g 223	1 |- ( A = B -> ( C = A <-> C = B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqeq2i  2207  eqeq2d  2208  eqeq12  2209  eleq1  2259  neeq2  2381  alexeq  2890  ceqex  2891  pm13.183  2902  eqeu  2934  mo2icl  2943  mob2  2944  euind  2951  reu6i  2955  reuind  2969  sbc5  3013  csbiebg  3127  sneq  3634  preqr1g  3797  preqr1  3799  prel12  3802  preq12bg  3804  opth  4271  euotd  4288  ordtriexmid  4558  ontriexmidim  4559  wetriext  4614  tfisi  4624  ideqg  4818  resieq  4957  cnveqb  5126  cnveq0  5127  iota5  5241  funopg  5293  fneq2  5348  foeq3  5481  tz6.12f  5590  funbrfv  5602  fnbrfvb  5604  fvelimab  5620  elrnrexdm  5704  eufnfv  5796  f1veqaeq  5819  mpoeq123  5985  ovmpt4g  6049  ovi3  6064  ovg  6066  caovcang  6089  caovcan  6092  uchoice  6204  frecabcl  6466  nntri3or  6560  dcdifsnid  6571  nnaordex  6595  nnawordex  6596  ereq2  6609  eroveu  6694  2dom  6873  fundmen  6874  xpf1o  6914  nneneq  6927  tridc  6969  prfidceq  6998  tpfidceq  7000  fisseneq  7004  fidcenumlemrks  7028  supsnti  7080  isotilem  7081  updjud  7157  nninfwlpoimlemdc  7252  exmidontriimlem3  7306  exmidontriimlem4  7307  onntri35  7320  exmidapne  7343  nqtri3or  7480  ltexnqq  7492  aptisr  7863  srpospr  7867  map2psrprg  7889  axpre-apti  7969  nntopi  7978  subval  8235  eqord1  8527  divvalap  8718  nn0ind-raph  9460  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  sqrtrval  11182  summodclem2  11564  prodmodclem2  11759  divides  11971  dvdstr  12010  odd2np1lem  12054  ndvdssub  12112  bitsinv1  12144  eucalglt  12250  hashgcdeq  12433  ennnfonelemim  12666  imasaddfnlemg  13016  dfgrp2  13229  grpidinv  13261  dfgrp3mlem  13300  isdomn  13901  xmeteq0  14679  mpodvdsmulf1o  15310  gausslemma2dlem0i  15382  trilpo  15774  trirec0  15775  redcwlpo  15786  redc0  15788  reap0  15789