Theorem eqeq2 2248

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqeq2i  2249  eqeq2d  2250  eqeq12  2251  eleq1  2301  neeq2  2434  alexeq  2952  ceqex  2953  pm13.183  2964  eqeu  2996  mo2icl  3005  mob2  3006  euind  3013  reu6i  3017  reuind  3031  sbc5  3075  csbiebg  3190  ifeqeqxdc  3687  sneq  3720  preqr1g  3891  preqr1  3893  prel12  3896  preq12bg  3898  opth  4379  euotd  4397  ordtriexmid  4670  ontriexmidim  4671  wetriext  4726  tfisi  4736  ideqg  4933  resieq  5075  cnveqb  5246  cnveq0  5247  iota5  5362  funopg  5414  fneq2  5473  foeq3  5616  tz6.12f  5727  funbrfv  5742  fnbrfvb  5744  fvelimab  5762  elrnrexdm  5850  eufnfv  5952  f1veqaeq  5978  mpoeq123  6150  ovmpt4g  6214  ovi3  6229  ovg  6231  caovcang  6254  caovcan  6257  uchoice  6375  suppssrst  6505  suppssrgst  6506  frecabcl  6674  nntri3or  6770  dcdifsnid  6781  nnaordex  6805  nnawordex  6806  ereq2  6819  eroveu  6904  2dom  7097  fundmen  7098  xpf1o  7148  nneneq  7162  tridc  7208  elssdc  7213  eqsndc  7214  prfidceq  7239  tpfidceq  7241  fisseneq  7246  fidcenumlemrks  7275  supsnti  7351  isotilem  7352  updjud  7428  nninfwlpoimlemdc  7523  exmidontriimlem3  7585  exmidontriimlem4  7586  onntri35  7602  exmidapne  7632  nqtri3or  7769  ltexnqq  7781  aptisr  8152  srpospr  8156  map2psrprg  8178  axpre-apti  8258  nntopi  8267  subval  8525  eqord1  8818  divvalap  9012  nn0ind-raph  9774  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  hashfibclem  11304  hashfibc  11305  wrdind  11516  wrd2ind  11517  reuccatpfxs1lem  11540  sqrtrval  11788  summodclem2  12174  prodmodclem2  12369  divides  12581  dvdstr  12620  odd2np1lem  12664  ndvdssub  12722  bitsinv1  12754  eucalglt  12860  hashgcdeq  13047  ennnfonelemim  13373  imasaddfnlemg  13694  dfgrp2  13891  grpidinv  13923  dfgrp3mlem  13962  isdomn  14687  xmeteq0  15585  mpodvdsmulf1o  16284  gausslemma2dlem0i  16381  upgredgpr  16595  ushgredgedg  16672  ushgredgedgloop  16674  uspgr2wlkeq  16811  clwwlkng  16851  clwwlkext2edg  16868  clwwlknon  16875  clwwlk0on0  16877  pw1dceq  17240  trilpo  17299  trirec0  17300  redcwlpo  17312  redc0  17314  reap0  17315