Theorem eqeq2 2187

Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eqeq2	⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Proof of Theorem eqeq2

Step	Hyp	Ref	Expression
1		eqeq1 2184	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqcom 2179	. 2 ⊢ (𝐶 = 𝐴 ↔ 𝐴 = 𝐶)
3		eqcom 2179	. 2 ⊢ (𝐶 = 𝐵 ↔ 𝐵 = 𝐶)
4	1, 2, 3	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

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  2865  ceqex  2866  pm13.183  2877  eqeu  2909  mo2icl  2918  mob2  2919  euind  2926  reu6i  2930  reuind  2944  sbc5  2988  csbiebg  3101  sneq  3605  preqr1g  3768  preqr1  3770  prel12  3773  preq12bg  3775  opth  4239  euotd  4256  ordtriexmid  4522  ontriexmidim  4523  wetriext  4578  tfisi  4588  ideqg  4780  resieq  4919  cnveqb  5086  cnveq0  5087  iota5  5200  funopg  5252  fneq2  5307  foeq3  5438  tz6.12f  5546  funbrfv  5556  fnbrfvb  5558  fvelimab  5574  elrnrexdm  5657  eufnfv  5749  f1veqaeq  5772  mpoeq123  5936  ovmpt4g  5999  ovi3  6013  ovg  6015  caovcang  6038  caovcan  6041  frecabcl  6402  nntri3or  6496  dcdifsnid  6507  nnaordex  6531  nnawordex  6532  ereq2  6545  eroveu  6628  2dom  6807  fundmen  6808  xpf1o  6846  nneneq  6859  tridc  6901  fisseneq  6933  fidcenumlemrks  6954  supsnti  7006  isotilem  7007  updjud  7083  nninfwlpoimlemdc  7177  exmidontriimlem3  7224  exmidontriimlem4  7225  onntri35  7238  exmidapne  7261  nqtri3or  7397  ltexnqq  7409  aptisr  7780  srpospr  7784  map2psrprg  7806  axpre-apti  7886  nntopi  7895  subval  8151  eqord1  8442  divvalap  8633  nn0ind-raph  9372  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  sqrtrval  11011  summodclem2  11392  prodmodclem2  11587  divides  11798  dvdstr  11837  odd2np1lem  11879  ndvdssub  11937  eucalglt  12059  hashgcdeq  12241  ennnfonelemim  12427  imasaddfnlemg  12740  dfgrp2  12907  grpidinv  12934  dfgrp3mlem  12973  xmeteq0  13898  trilpo  14830  trirec0  14831  redcwlpo  14842  redc0  14844  reap0  14845