Theorem eqeq2 2217

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 2214	. 2 |- ( A = B -> ( A = C <-> B = C ) )
2		eqcom 2209	. 2 |- ( C = A <-> A = C )
3		eqcom 2209	. 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 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  eqeq2i  2218  eqeq2d  2219  eqeq12  2220  eleq1  2270  neeq2  2392  alexeq  2906  ceqex  2907  pm13.183  2918  eqeu  2950  mo2icl  2959  mob2  2960  euind  2967  reu6i  2971  reuind  2985  sbc5  3029  csbiebg  3144  sneq  3654  preqr1g  3820  preqr1  3822  prel12  3825  preq12bg  3827  opth  4299  euotd  4317  ordtriexmid  4587  ontriexmidim  4588  wetriext  4643  tfisi  4653  ideqg  4847  resieq  4988  cnveqb  5157  cnveq0  5158  iota5  5272  funopg  5324  fneq2  5382  foeq3  5518  tz6.12f  5628  funbrfv  5640  fnbrfvb  5642  fvelimab  5658  elrnrexdm  5742  eufnfv  5838  f1veqaeq  5861  mpoeq123  6027  ovmpt4g  6091  ovi3  6106  ovg  6108  caovcang  6131  caovcan  6134  uchoice  6246  frecabcl  6508  nntri3or  6602  dcdifsnid  6613  nnaordex  6637  nnawordex  6638  ereq2  6651  eroveu  6736  2dom  6921  fundmen  6922  xpf1o  6966  nneneq  6979  tridc  7022  prfidceq  7051  tpfidceq  7053  fisseneq  7057  fidcenumlemrks  7081  supsnti  7133  isotilem  7134  updjud  7210  nninfwlpoimlemdc  7305  exmidontriimlem3  7366  exmidontriimlem4  7367  onntri35  7383  exmidapne  7407  nqtri3or  7544  ltexnqq  7556  aptisr  7927  srpospr  7931  map2psrprg  7953  axpre-apti  8033  nntopi  8042  subval  8299  eqord1  8591  divvalap  8782  nn0ind-raph  9525  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  wrdind  11213  wrd2ind  11214  reuccatpfxs1lem  11237  sqrtrval  11426  summodclem2  11808  prodmodclem2  12003  divides  12215  dvdstr  12254  odd2np1lem  12298  ndvdssub  12356  bitsinv1  12388  eucalglt  12494  hashgcdeq  12677  ennnfonelemim  12910  imasaddfnlemg  13261  dfgrp2  13474  grpidinv  13506  dfgrp3mlem  13545  isdomn  14146  xmeteq0  14946  mpodvdsmulf1o  15577  gausslemma2dlem0i  15649  upgredgpr  15853  trilpo  16184  trirec0  16185  redcwlpo  16196  redc0  16198  reap0  16199