Theorem cleq2d 1112

Description: Deduction from equality to equivalence of equalities.

Hypothesis

Ref	Expression
cleq2d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
cleq2d	⊢ (φ → (C = A ↔ C = B))

Proof of Theorem cleq2d

Step	Hyp	Ref	Expression
1		cleq2d.1	. 2 ⊢ (φ → A = B)
2		cleq2 1110	. 2 ⊢ (A = B → (C = A ↔ C = B))
3	1, 2	syl 12	1 ⊢ (φ → (C = A ↔ C = B))

Syntax hints:   → wi 2   ↔ wb 127   = wceq 1091

This theorem is referenced by:  cleq12d 1115  eqtrd 1128  cleq2tr 1148  opthg 1899  eqvinop 1901  moop2 1910  eusn 1913  opabid 2099  cbvopab 2104  cbvopab1 2106  cbvopab1s 2107  cbvopab1v 2108  cbvopab2v 2109  limeq 2211  onuninsuc 2356  elxp4 2640  elxp5 2641  funcnvuni 2706  fnopabfv 2858  fvopab4g 2870  fvopabn 2873  abrexexlem1 2910  abrexexlem2 2911  abrexex 2912  f1fvf 2917  f1fveq 2918  f1ocnvfv 2921  f1ocnvfvb 2922  tz7.44-2 2967  tz7.44-3 2968  rdgeq1 2972  rdgeq2 2973  rdglem2 2976  tz7.48lem 2993  dfoprab2 3021  cbvoprab12 3028  fnoprval 3042  oprabval2g 3050  oprabval3 3052  oprabval4g 3053  oprvalex 3055  caoprcan 3069  fo1st 3094  fo2nd 3095  omv 3120  oev 3122  oe1m 3147  qseq2 3226  ecelqsi 3229  snec 3232  ecoptocl 3239  th3qlem1 3250  th3qlem2 3251  th3q 3253  en1 3331  mapsnen 3334  xpsnen 3339  xpassen 3344  pw2en 3348  mapxpen 3390  xpmapenlem3 3393  xpmapenlem4 3394  xpmapenlem5 3395  mapunen 3397  unfilem3 3440  tz9.12lem1 3503  tz9.12lem3 3505  rankr1g 3519  aceq3lem 3555  aceq5lem1 3558  aceq5lem4 3561  aceq6b 3565  kmlem8 3587  oncard 3636  cardalephex 3691  cf0 3705  cflecard 3707  cfsuc 3709  indpi 3828  genpv 3896  genpprecl 3898  genpass 3906  distrlem1pr 3921  distrlem5pr 3925  1idpr 3927  axcnre 4087  addcant 4122  mulcant 4208  rec11 4262  cru 4529  crut 4531  creur 4532  creui 4533  nn0ind 4612  znq 4630  zqt 4632  qaddclt 4642  qnegclt 4643  qmulclt 4644  qrecclt 4646  seqlem1 4662  seqval 4665  seqsuclem 4669  sqe11t 4705  nn0opth2t 4726  sqrsq 4764  sqr2irrlem2 4778  sqr2irrlem3 4779  sqr2irrlem5 4781  replimt 4798  ruclem12 4896  ruclem13 4897  nn0ennn 4925  znnenlem 4929  projlem8 5200  projlem10 5202  projlem15 5207  pjthlem14 5238  pjthu 5241  pjthu2 5242  pjmvalt 5245  omlsi 5250  pjpj0 5259  axpjpjt 5260  pjpjtht 5262  shscl 5282  shscomt 5284  shsvat 5285  dfchsup2 5299  dfchj2 5325  dfchj3 5326  shunss 5338  h1de2ctlem 5460  elspansnt 5471  elspansn2t 5472  spansncol 5473  spanunsn 5482  h1datomt 5484  hosmvalt 5487  hodmvalt 5488  cmbrt 5494  osumlem5 5534  spansncv 5542  spansncvt 5543  pjjs 5585  pjrn 5587  atom1d 5750  sumdmdlem 5786

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