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  3765  preqr1  3767  prel12  3770  preq12bg  3772  opth  4235  euotd  4252  ordtriexmid  4518  ontriexmidim  4519  wetriext  4574  tfisi  4584  ideqg  4775  resieq  4914  cnveqb  5081  cnveq0  5082  iota5  5195  funopg  5247  fneq2  5302  foeq3  5433  tz6.12f  5541  funbrfv  5551  fnbrfvb  5553  fvelimab  5569  elrnrexdm  5652  eufnfv  5743  f1veqaeq  5765  mpoeq123  5929  ovmpt4g  5992  ovi3  6006  ovg  6008  caovcang  6031  caovcan  6034  frecabcl  6395  nntri3or  6489  dcdifsnid  6500  nnaordex  6524  nnawordex  6525  ereq2  6538  eroveu  6621  2dom  6800  fundmen  6801  xpf1o  6839  nneneq  6852  tridc  6894  fisseneq  6926  fidcenumlemrks  6947  supsnti  6999  isotilem  7000  updjud  7076  nninfwlpoimlemdc  7170  exmidontriimlem3  7217  exmidontriimlem4  7218  onntri35  7231  exmidapne  7254  nqtri3or  7390  ltexnqq  7402  aptisr  7773  srpospr  7777  map2psrprg  7799  axpre-apti  7879  nntopi  7888  subval  8143  eqord1  8434  divvalap  8625  nn0ind-raph  9364  frecuzrdgtcl  10405  frecuzrdgfunlem  10412  sqrtrval  11000  summodclem2  11381  prodmodclem2  11576  divides  11787  dvdstr  11826  odd2np1lem  11867  ndvdssub  11925  eucalglt  12047  hashgcdeq  12229  ennnfonelemim  12415  dfgrp2  12830  grpidinv  12857  dfgrp3mlem  12896  xmeteq0  13641  trilpo  14562  trirec0  14563  redcwlpo  14574  redc0  14576  reap0  14577