Theorem eqeq2 2239

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 2236	. 2 |- ( A = B -> ( A = C <-> B = C ) )
2		eqcom 2231	. 2 |- ( C = A <-> A = C )
3		eqcom 2231	. 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 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqeq2i  2240  eqeq2d  2241  eqeq12  2242  eleq1  2292  neeq2  2414  alexeq  2929  ceqex  2930  pm13.183  2941  eqeu  2973  mo2icl  2982  mob2  2983  euind  2990  reu6i  2994  reuind  3008  sbc5  3052  csbiebg  3167  sneq  3677  preqr1g  3844  preqr1  3846  prel12  3849  preq12bg  3851  opth  4323  euotd  4341  ordtriexmid  4613  ontriexmidim  4614  wetriext  4669  tfisi  4679  ideqg  4873  resieq  5015  cnveqb  5184  cnveq0  5185  iota5  5300  funopg  5352  fneq2  5410  foeq3  5546  tz6.12f  5656  funbrfv  5670  fnbrfvb  5672  fvelimab  5690  elrnrexdm  5774  eufnfv  5870  f1veqaeq  5893  mpoeq123  6063  ovmpt4g  6127  ovi3  6142  ovg  6144  caovcang  6167  caovcan  6170  uchoice  6283  frecabcl  6545  nntri3or  6639  dcdifsnid  6650  nnaordex  6674  nnawordex  6675  ereq2  6688  eroveu  6773  2dom  6958  fundmen  6959  xpf1o  7005  nneneq  7018  tridc  7061  prfidceq  7090  tpfidceq  7092  fisseneq  7096  fidcenumlemrks  7120  supsnti  7172  isotilem  7173  updjud  7249  nninfwlpoimlemdc  7344  exmidontriimlem3  7405  exmidontriimlem4  7406  onntri35  7422  exmidapne  7446  nqtri3or  7583  ltexnqq  7595  aptisr  7966  srpospr  7970  map2psrprg  7992  axpre-apti  8072  nntopi  8081  subval  8338  eqord1  8630  divvalap  8821  nn0ind-raph  9564  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  wrdind  11254  wrd2ind  11255  reuccatpfxs1lem  11278  sqrtrval  11511  summodclem2  11893  prodmodclem2  12088  divides  12300  dvdstr  12339  odd2np1lem  12383  ndvdssub  12441  bitsinv1  12473  eucalglt  12579  hashgcdeq  12762  ennnfonelemim  12995  imasaddfnlemg  13347  dfgrp2  13560  grpidinv  13592  dfgrp3mlem  13631  isdomn  14233  xmeteq0  15033  mpodvdsmulf1o  15664  gausslemma2dlem0i  15736  upgredgpr  15947  ushgredgedg  16024  ushgredgedgloop  16026  uspgr2wlkeq  16076  trilpo  16411  trirec0  16412  redcwlpo  16423  redc0  16425  reap0  16426