Theorem eqeq2 2206

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqeq2i  2207  eqeq2d  2208  eqeq12  2209  eleq1  2259  neeq2  2381  alexeq  2890  ceqex  2891  pm13.183  2902  eqeu  2934  mo2icl  2943  mob2  2944  euind  2951  reu6i  2955  reuind  2969  sbc5  3013  csbiebg  3127  sneq  3633  preqr1g  3796  preqr1  3798  prel12  3801  preq12bg  3803  opth  4270  euotd  4287  ordtriexmid  4557  ontriexmidim  4558  wetriext  4613  tfisi  4623  ideqg  4817  resieq  4956  cnveqb  5125  cnveq0  5126  iota5  5240  funopg  5292  fneq2  5347  foeq3  5478  tz6.12f  5587  funbrfv  5599  fnbrfvb  5601  fvelimab  5617  elrnrexdm  5701  eufnfv  5793  f1veqaeq  5816  mpoeq123  5981  ovmpt4g  6045  ovi3  6060  ovg  6062  caovcang  6085  caovcan  6088  uchoice  6195  frecabcl  6457  nntri3or  6551  dcdifsnid  6562  nnaordex  6586  nnawordex  6587  ereq2  6600  eroveu  6685  2dom  6864  fundmen  6865  xpf1o  6905  nneneq  6918  tridc  6960  prfidceq  6989  tpfidceq  6991  fisseneq  6995  fidcenumlemrks  7019  supsnti  7071  isotilem  7072  updjud  7148  nninfwlpoimlemdc  7243  exmidontriimlem3  7290  exmidontriimlem4  7291  onntri35  7304  exmidapne  7327  nqtri3or  7463  ltexnqq  7475  aptisr  7846  srpospr  7850  map2psrprg  7872  axpre-apti  7952  nntopi  7961  subval  8218  eqord1  8510  divvalap  8701  nn0ind-raph  9443  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  sqrtrval  11165  summodclem2  11547  prodmodclem2  11742  divides  11954  dvdstr  11993  odd2np1lem  12037  ndvdssub  12095  eucalglt  12225  hashgcdeq  12408  ennnfonelemim  12641  imasaddfnlemg  12957  dfgrp2  13159  grpidinv  13191  dfgrp3mlem  13230  isdomn  13825  xmeteq0  14595  mpodvdsmulf1o  15226  gausslemma2dlem0i  15298  trilpo  15687  trirec0  15688  redcwlpo  15699  redc0  15701  reap0  15702