Theorem eqeq2 2199

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 2196	. 2 |- ( A = B -> ( A = C <-> B = C ) )
2		eqcom 2191	. 2 |- ( C = A <-> A = C )
3		eqcom 2191	. 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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  eqeq2i  2200  eqeq2d  2201  eqeq12  2202  eleq1  2252  neeq2  2374  alexeq  2878  ceqex  2879  pm13.183  2890  eqeu  2922  mo2icl  2931  mob2  2932  euind  2939  reu6i  2943  reuind  2957  sbc5  3001  csbiebg  3114  sneq  3618  preqr1g  3781  preqr1  3783  prel12  3786  preq12bg  3788  opth  4255  euotd  4272  ordtriexmid  4538  ontriexmidim  4539  wetriext  4594  tfisi  4604  ideqg  4796  resieq  4935  cnveqb  5102  cnveq0  5103  iota5  5217  funopg  5269  fneq2  5324  foeq3  5455  tz6.12f  5563  funbrfv  5574  fnbrfvb  5576  fvelimab  5592  elrnrexdm  5675  eufnfv  5767  f1veqaeq  5790  mpoeq123  5954  ovmpt4g  6018  ovi3  6032  ovg  6034  caovcang  6057  caovcan  6060  frecabcl  6423  nntri3or  6517  dcdifsnid  6528  nnaordex  6552  nnawordex  6553  ereq2  6566  eroveu  6651  2dom  6830  fundmen  6831  xpf1o  6871  nneneq  6884  tridc  6926  fisseneq  6959  fidcenumlemrks  6981  supsnti  7033  isotilem  7034  updjud  7110  nninfwlpoimlemdc  7204  exmidontriimlem3  7251  exmidontriimlem4  7252  onntri35  7265  exmidapne  7288  nqtri3or  7424  ltexnqq  7436  aptisr  7807  srpospr  7811  map2psrprg  7833  axpre-apti  7913  nntopi  7922  subval  8178  eqord1  8469  divvalap  8660  nn0ind-raph  9399  frecuzrdgtcl  10442  frecuzrdgfunlem  10449  sqrtrval  11040  summodclem2  11421  prodmodclem2  11616  divides  11827  dvdstr  11866  odd2np1lem  11908  ndvdssub  11966  eucalglt  12088  hashgcdeq  12270  ennnfonelemim  12474  imasaddfnlemg  12788  dfgrp2  12968  grpidinv  13000  dfgrp3mlem  13039  xmeteq0  14311  trilpo  15245  trirec0  15246  redcwlpo  15257  redc0  15259  reap0  15260