Theorem eqeq2 2187

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 2184	. 2 |- ( A = B -> ( A = C <-> B = C ) )
2		eqcom 2179	. 2 |- ( C = A <-> A = C )
3		eqcom 2179	. 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 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqeq2i  2188  eqeq2d  2189  eqeq12  2190  eleq1  2240  neeq2  2361  alexeq  2864  ceqex  2865  pm13.183  2876  eqeu  2908  mo2icl  2917  mob2  2918  euind  2925  reu6i  2929  reuind  2943  sbc5  2987  csbiebg  3100  sneq  3604  preqr1g  3767  preqr1  3769  prel12  3772  preq12bg  3774  opth  4238  euotd  4255  ordtriexmid  4521  ontriexmidim  4522  wetriext  4577  tfisi  4587  ideqg  4779  resieq  4918  cnveqb  5085  cnveq0  5086  iota5  5199  funopg  5251  fneq2  5306  foeq3  5437  tz6.12f  5545  funbrfv  5555  fnbrfvb  5557  fvelimab  5573  elrnrexdm  5656  eufnfv  5748  f1veqaeq  5770  mpoeq123  5934  ovmpt4g  5997  ovi3  6011  ovg  6013  caovcang  6036  caovcan  6039  frecabcl  6400  nntri3or  6494  dcdifsnid  6505  nnaordex  6529  nnawordex  6530  ereq2  6543  eroveu  6626  2dom  6805  fundmen  6806  xpf1o  6844  nneneq  6857  tridc  6899  fisseneq  6931  fidcenumlemrks  6952  supsnti  7004  isotilem  7005  updjud  7081  nninfwlpoimlemdc  7175  exmidontriimlem3  7222  exmidontriimlem4  7223  onntri35  7236  exmidapne  7259  nqtri3or  7395  ltexnqq  7407  aptisr  7778  srpospr  7782  map2psrprg  7804  axpre-apti  7884  nntopi  7893  subval  8149  eqord1  8440  divvalap  8631  nn0ind-raph  9370  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  sqrtrval  11009  summodclem2  11390  prodmodclem2  11585  divides  11796  dvdstr  11835  odd2np1lem  11877  ndvdssub  11935  eucalglt  12057  hashgcdeq  12239  ennnfonelemim  12425  imasaddfnlemg  12735  dfgrp2  12902  grpidinv  12929  dfgrp3mlem  12968  xmeteq0  13862  trilpo  14794  trirec0  14795  redcwlpo  14806  redc0  14808  reap0  14809