Theorem eqeq2 2215

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 2212	. 2 |- ( A = B -> ( A = C <-> B = C ) )
2		eqcom 2207	. 2 |- ( C = A <-> A = C )
3		eqcom 2207	. 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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  eqeq2i  2216  eqeq2d  2217  eqeq12  2218  eleq1  2268  neeq2  2390  alexeq  2899  ceqex  2900  pm13.183  2911  eqeu  2943  mo2icl  2952  mob2  2953  euind  2960  reu6i  2964  reuind  2978  sbc5  3022  csbiebg  3136  sneq  3644  preqr1g  3807  preqr1  3809  prel12  3812  preq12bg  3814  opth  4281  euotd  4299  ordtriexmid  4569  ontriexmidim  4570  wetriext  4625  tfisi  4635  ideqg  4829  resieq  4969  cnveqb  5138  cnveq0  5139  iota5  5253  funopg  5305  fneq2  5363  foeq3  5496  tz6.12f  5605  funbrfv  5617  fnbrfvb  5619  fvelimab  5635  elrnrexdm  5719  eufnfv  5815  f1veqaeq  5838  mpoeq123  6004  ovmpt4g  6068  ovi3  6083  ovg  6085  caovcang  6108  caovcan  6111  uchoice  6223  frecabcl  6485  nntri3or  6579  dcdifsnid  6590  nnaordex  6614  nnawordex  6615  ereq2  6628  eroveu  6713  2dom  6897  fundmen  6898  xpf1o  6941  nneneq  6954  tridc  6996  prfidceq  7025  tpfidceq  7027  fisseneq  7031  fidcenumlemrks  7055  supsnti  7107  isotilem  7108  updjud  7184  nninfwlpoimlemdc  7279  exmidontriimlem3  7335  exmidontriimlem4  7336  onntri35  7349  exmidapne  7372  nqtri3or  7509  ltexnqq  7521  aptisr  7892  srpospr  7896  map2psrprg  7918  axpre-apti  7998  nntopi  8007  subval  8264  eqord1  8556  divvalap  8747  nn0ind-raph  9490  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  sqrtrval  11311  summodclem2  11693  prodmodclem2  11888  divides  12100  dvdstr  12139  odd2np1lem  12183  ndvdssub  12241  bitsinv1  12273  eucalglt  12379  hashgcdeq  12562  ennnfonelemim  12795  imasaddfnlemg  13146  dfgrp2  13359  grpidinv  13391  dfgrp3mlem  13430  isdomn  14031  xmeteq0  14831  mpodvdsmulf1o  15462  gausslemma2dlem0i  15534  trilpo  15986  trirec0  15987  redcwlpo  15998  redc0  16000  reap0  16001