Theorem eqeq2 2244

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

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

This theorem is referenced by:  eqeq2i  2245  eqeq2d  2246  eqeq12  2247  eleq1  2297  neeq2  2428  alexeq  2945  ceqex  2946  pm13.183  2957  eqeu  2989  mo2icl  2998  mob2  2999  euind  3006  reu6i  3010  reuind  3024  sbc5  3068  csbiebg  3183  sneq  3702  preqr1g  3872  preqr1  3874  prel12  3877  preq12bg  3879  opth  4355  euotd  4373  ordtriexmid  4645  ontriexmidim  4646  wetriext  4701  tfisi  4711  ideqg  4908  resieq  5050  cnveqb  5220  cnveq0  5221  iota5  5336  funopg  5388  fneq2  5447  foeq3  5590  tz6.12f  5701  funbrfv  5715  fnbrfvb  5717  fvelimab  5735  elrnrexdm  5818  eufnfv  5919  f1veqaeq  5944  mpoeq123  6114  ovmpt4g  6178  ovi3  6193  ovg  6195  caovcang  6218  caovcan  6221  uchoice  6333  suppssrst  6463  suppssrgst  6464  frecabcl  6632  nntri3or  6728  dcdifsnid  6739  nnaordex  6763  nnawordex  6764  ereq2  6777  eroveu  6862  2dom  7048  fundmen  7049  xpf1o  7099  nneneq  7113  tridc  7159  elssdc  7164  eqsndc  7165  prfidceq  7190  tpfidceq  7192  fisseneq  7197  fidcenumlemrks  7225  supsnti  7298  isotilem  7299  updjud  7375  nninfwlpoimlemdc  7470  exmidontriimlem3  7532  exmidontriimlem4  7533  onntri35  7549  exmidapne  7576  nqtri3or  7713  ltexnqq  7725  aptisr  8096  srpospr  8100  map2psrprg  8122  axpre-apti  8202  nntopi  8211  subval  8467  eqord1  8759  divvalap  8950  nn0ind-raph  9698  frecuzrdgtcl  10778  frecuzrdgfunlem  10785  hashfibclem  11210  hashfibc  11211  wrdind  11418  wrd2ind  11419  reuccatpfxs1lem  11442  sqrtrval  11689  summodclem2  12072  prodmodclem2  12267  divides  12479  dvdstr  12518  odd2np1lem  12562  ndvdssub  12620  bitsinv1  12652  eucalglt  12758  hashgcdeq  12941  ennnfonelemim  13192  imasaddfnlemg  13544  dfgrp2  13757  grpidinv  13789  dfgrp3mlem  13828  isdomn  14432  xmeteq0  15241  mpodvdsmulf1o  15875  gausslemma2dlem0i  15947  upgredgpr  16161  ushgredgedg  16238  ushgredgedgloop  16240  uspgr2wlkeq  16377  clwwlkng  16417  clwwlkext2edg  16434  clwwlknon  16441  clwwlk0on0  16443  pw1dceq  16795  trilpo  16844  trirec0  16845  redcwlpo  16857  redc0  16859  reap0  16860