Theorem eqeq2 2241

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 2238	. 2 |- ( A = B -> ( A = C <-> B = C ) )
2		eqcom 2233	. 2 |- ( C = A <-> A = C )
3		eqcom 2233	. 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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  eqeq2i  2242  eqeq2d  2243  eqeq12  2244  eleq1  2294  neeq2  2417  alexeq  2933  ceqex  2934  pm13.183  2945  eqeu  2977  mo2icl  2986  mob2  2987  euind  2994  reu6i  2998  reuind  3012  sbc5  3056  csbiebg  3171  sneq  3684  preqr1g  3854  preqr1  3856  prel12  3859  preq12bg  3861  opth  4335  euotd  4353  ordtriexmid  4625  ontriexmidim  4626  wetriext  4681  tfisi  4691  ideqg  4887  resieq  5029  cnveqb  5199  cnveq0  5200  iota5  5315  funopg  5367  fneq2  5426  foeq3  5566  tz6.12f  5677  funbrfv  5691  fnbrfvb  5693  fvelimab  5711  elrnrexdm  5794  eufnfv  5895  f1veqaeq  5920  mpoeq123  6090  ovmpt4g  6154  ovi3  6169  ovg  6171  caovcang  6194  caovcan  6197  uchoice  6309  suppssrst  6439  suppssrgst  6440  frecabcl  6608  nntri3or  6704  dcdifsnid  6715  nnaordex  6739  nnawordex  6740  ereq2  6753  eroveu  6838  2dom  7023  fundmen  7024  xpf1o  7073  nneneq  7086  tridc  7132  elssdc  7137  eqsndc  7138  prfidceq  7163  tpfidceq  7165  fisseneq  7170  fidcenumlemrks  7195  supsnti  7264  isotilem  7265  updjud  7341  nninfwlpoimlemdc  7436  exmidontriimlem3  7498  exmidontriimlem4  7499  onntri35  7515  exmidapne  7539  nqtri3or  7676  ltexnqq  7688  aptisr  8059  srpospr  8063  map2psrprg  8085  axpre-apti  8165  nntopi  8174  subval  8430  eqord1  8722  divvalap  8913  nn0ind-raph  9658  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  wrdind  11369  wrd2ind  11370  reuccatpfxs1lem  11393  sqrtrval  11640  summodclem2  12023  prodmodclem2  12218  divides  12430  dvdstr  12469  odd2np1lem  12513  ndvdssub  12571  bitsinv1  12603  eucalglt  12709  hashgcdeq  12892  ennnfonelemim  13125  imasaddfnlemg  13477  dfgrp2  13690  grpidinv  13722  dfgrp3mlem  13761  isdomn  14365  xmeteq0  15170  mpodvdsmulf1o  15804  gausslemma2dlem0i  15876  upgredgpr  16090  ushgredgedg  16167  ushgredgedgloop  16169  uspgr2wlkeq  16306  clwwlkng  16346  clwwlkext2edg  16363  clwwlknon  16370  clwwlk0on0  16372  pw1dceq  16726  trilpo  16775  trirec0  16776  redcwlpo  16788  redc0  16790  reap0  16791