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  4282  euotd  4300  ordtriexmid  4570  ontriexmidim  4571  wetriext  4626  tfisi  4636  ideqg  4830  resieq  4970  cnveqb  5139  cnveq0  5140  iota5  5254  funopg  5306  fneq2  5364  foeq3  5498  tz6.12f  5607  funbrfv  5619  fnbrfvb  5621  fvelimab  5637  elrnrexdm  5721  eufnfv  5817  f1veqaeq  5840  mpoeq123  6006  ovmpt4g  6070  ovi3  6085  ovg  6087  caovcang  6110  caovcan  6113  uchoice  6225  frecabcl  6487  nntri3or  6581  dcdifsnid  6592  nnaordex  6616  nnawordex  6617  ereq2  6630  eroveu  6715  2dom  6899  fundmen  6900  xpf1o  6943  nneneq  6956  tridc  6998  prfidceq  7027  tpfidceq  7029  fisseneq  7033  fidcenumlemrks  7057  supsnti  7109  isotilem  7110  updjud  7186  nninfwlpoimlemdc  7281  exmidontriimlem3  7337  exmidontriimlem4  7338  onntri35  7351  exmidapne  7374  nqtri3or  7511  ltexnqq  7523  aptisr  7894  srpospr  7898  map2psrprg  7920  axpre-apti  8000  nntopi  8009  subval  8266  eqord1  8558  divvalap  8749  nn0ind-raph  9492  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  sqrtrval  11344  summodclem2  11726  prodmodclem2  11921  divides  12133  dvdstr  12172  odd2np1lem  12216  ndvdssub  12274  bitsinv1  12306  eucalglt  12412  hashgcdeq  12595  ennnfonelemim  12828  imasaddfnlemg  13179  dfgrp2  13392  grpidinv  13424  dfgrp3mlem  13463  isdomn  14064  xmeteq0  14864  mpodvdsmulf1o  15495  gausslemma2dlem0i  15567  trilpo  16019  trirec0  16020  redcwlpo  16031  redc0  16033  reap0  16034