Theorem eqeq2 2174

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 2171	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqcom 2166	. 2 ⊢ (𝐶 = 𝐴 ↔ 𝐴 = 𝐶)
3		eqcom 2166	. 2 ⊢ (𝐶 = 𝐵 ↔ 𝐵 = 𝐶)
4	1, 2, 3	3bitr4g 222	1 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-cleq 2157

This theorem is referenced by:  eqeq2i  2175  eqeq2d  2176  eqeq12  2177  eleq1  2227  neeq2  2348  alexeq  2847  ceqex  2848  pm13.183  2859  eqeu  2891  mo2icl  2900  mob2  2901  euind  2908  reu6i  2912  reuind  2926  sbc5  2969  csbiebg  3082  sneq  3581  preqr1g  3740  preqr1  3742  prel12  3745  preq12bg  3747  opth  4209  euotd  4226  ordtriexmid  4492  ontriexmidim  4493  wetriext  4548  tfisi  4558  ideqg  4749  resieq  4888  cnveqb  5053  cnveq0  5054  iota5  5167  funopg  5216  fneq2  5271  foeq3  5402  tz6.12f  5509  funbrfv  5519  fnbrfvb  5521  fvelimab  5536  elrnrexdm  5618  eufnfv  5709  f1veqaeq  5731  mpoeq123  5892  ovmpt4g  5955  ovi3  5969  ovg  5971  caovcang  5994  caovcan  5997  frecabcl  6358  nntri3or  6452  dcdifsnid  6463  nnaordex  6486  nnawordex  6487  ereq2  6500  eroveu  6583  2dom  6762  fundmen  6763  xpf1o  6801  nneneq  6814  tridc  6856  fisseneq  6888  fidcenumlemrks  6909  supsnti  6961  isotilem  6962  updjud  7038  exmidontriimlem3  7170  exmidontriimlem4  7171  onntri35  7184  nqtri3or  7328  ltexnqq  7340  aptisr  7711  srpospr  7715  map2psrprg  7737  axpre-apti  7817  nntopi  7826  subval  8081  eqord1  8372  divvalap  8561  nn0ind-raph  9299  frecuzrdgtcl  10337  frecuzrdgfunlem  10344  sqrtrval  10928  summodclem2  11309  prodmodclem2  11504  divides  11715  dvdstr  11754  odd2np1lem  11794  ndvdssub  11852  eucalglt  11968  hashgcdeq  12148  ennnfonelemim  12294  xmeteq0  12900  trilpo  13756  trirec0  13757  redcwlpo  13768  redc0  13770  reap0  13771