Theorem cleq2i 1111

Description: Inference from equality to equivalence of equalities.

Hypothesis

Ref	Expression
cleq2i.1	⊢ A = B

Assertion

Ref	Expression
cleq2i	⊢ (C = A ↔ C = B)

Proof of Theorem cleq2i

Step	Hyp	Ref	Expression
1		cleq2i.1	. 2 ⊢ A = B
2		cleq2 1110	. 2 ⊢ (A = B → (C = A ↔ C = B))
3	1, 2	ax-mp 6	1 ⊢ (C = A ↔ C = B)

Syntax hints:   ↔ wb 127   = wceq 1091

This theorem is referenced by:  cleq12i 1114  eqtr 1119  rabid2 1309  dfss2 1497  ssequn1 1628  pwex 1806  preq12b 1874  opprc3 1908  wefrc 2195  orddif 2326  onuninsuc 2356  funimaexg 2715  fnressn 2897  fressnfv 2898  fvresex 2909  abrexexlem2 2911  rdgsucopab 2984  rdgsucopabn 2985  frsucopab 2992  fnoprval 3042  elxp6 3093  0ne1oOLD 3113  qsid 3237  rankr1 3518  ac6lem 3575  cardeq0 3639  cf0 3705  addcompr 3917  mulcompr 3919  axrecex 4079  axrnegex 4080  axrrecex 4081  mul0or 4210  negne0 4379  sqr00t 4770  sqr2irrlem4 4780  chnle 5406  h1de2ctlem 5460  cmcmlem 5500  cmcm2 5502  cmbr2 5505  pjss2 5571  pjclem1 5649  jplem1 5701

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org