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  4377  euotd  4395  ordtriexmid  4668  ontriexmidim  4669  wetriext  4724  tfisi  4734  ideqg  4931  resieq  5073  cnveqb  5243  cnveq0  5244  iota5  5359  funopg  5411  fneq2  5470  foeq3  5613  tz6.12f  5724  funbrfv  5739  fnbrfvb  5741  fvelimab  5759  elrnrexdm  5847  eufnfv  5949  f1veqaeq  5975  mpoeq123  6147  ovmpt4g  6211  ovi3  6226  ovg  6228  caovcang  6251  caovcan  6254  uchoice  6371  suppssrst  6501  suppssrgst  6502  frecabcl  6670  nntri3or  6766  dcdifsnid  6777  nnaordex  6801  nnawordex  6802  ereq2  6815  eroveu  6900  2dom  7093  fundmen  7094  xpf1o  7144  nneneq  7158  tridc  7204  elssdc  7209  eqsndc  7210  prfidceq  7235  tpfidceq  7237  fisseneq  7242  fidcenumlemrks  7270  supsnti  7345  isotilem  7346  updjud  7422  nninfwlpoimlemdc  7517  exmidontriimlem3  7579  exmidontriimlem4  7580  onntri35  7596  exmidapne  7626  nqtri3or  7763  ltexnqq  7775  aptisr  8146  srpospr  8150  map2psrprg  8172  axpre-apti  8252  nntopi  8261  subval  8519  eqord1  8812  divvalap  9006  nn0ind-raph  9767  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  hashfibclem  11296  hashfibc  11297  wrdind  11508  wrd2ind  11509  reuccatpfxs1lem  11532  sqrtrval  11780  summodclem2  12165  prodmodclem2  12360  divides  12572  dvdstr  12611  odd2np1lem  12655  ndvdssub  12713  bitsinv1  12745  eucalglt  12851  hashgcdeq  13038  ennnfonelemim  13364  imasaddfnlemg  13684  dfgrp2  13881  grpidinv  13913  dfgrp3mlem  13952  isdomn  14627  xmeteq0  15509  mpodvdsmulf1o  16185  gausslemma2dlem0i  16274  upgredgpr  16488  ushgredgedg  16565  ushgredgedgloop  16567  uspgr2wlkeq  16704  clwwlkng  16744  clwwlkext2edg  16761  clwwlknon  16768  clwwlk0on0  16770  pw1dceq  17133  trilpo  17190  trirec0  17191  redcwlpo  17203  redc0  17205  reap0  17206