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  2863  ceqex  2864  pm13.183  2875  eqeu  2907  mo2icl  2916  mob2  2917  euind  2924  reu6i  2928  reuind  2942  sbc5  2986  csbiebg  3099  sneq  3603  preqr1g  3766  preqr1  3768  prel12  3771  preq12bg  3773  opth  4237  euotd  4254  ordtriexmid  4520  ontriexmidim  4521  wetriext  4576  tfisi  4586  ideqg  4778  resieq  4917  cnveqb  5084  cnveq0  5085  iota5  5198  funopg  5250  fneq2  5305  foeq3  5436  tz6.12f  5544  funbrfv  5554  fnbrfvb  5556  fvelimab  5572  elrnrexdm  5655  eufnfv  5747  f1veqaeq  5769  mpoeq123  5933  ovmpt4g  5996  ovi3  6010  ovg  6012  caovcang  6035  caovcan  6038  frecabcl  6399  nntri3or  6493  dcdifsnid  6504  nnaordex  6528  nnawordex  6529  ereq2  6542  eroveu  6625  2dom  6804  fundmen  6805  xpf1o  6843  nneneq  6856  tridc  6898  fisseneq  6930  fidcenumlemrks  6951  supsnti  7003  isotilem  7004  updjud  7080  nninfwlpoimlemdc  7174  exmidontriimlem3  7221  exmidontriimlem4  7222  onntri35  7235  exmidapne  7258  nqtri3or  7394  ltexnqq  7406  aptisr  7777  srpospr  7781  map2psrprg  7803  axpre-apti  7883  nntopi  7892  subval  8148  eqord1  8439  divvalap  8630  nn0ind-raph  9369  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  sqrtrval  11008  summodclem2  11389  prodmodclem2  11584  divides  11795  dvdstr  11834  odd2np1lem  11876  ndvdssub  11934  eucalglt  12056  hashgcdeq  12238  ennnfonelemim  12424  imasaddfnlemg  12734  dfgrp2  12901  grpidinv  12928  dfgrp3mlem  12967  xmeteq0  13829  trilpo  14761  trirec0  14762  redcwlpo  14773  redc0  14775  reap0  14776