Theorem cleq1d 1109

Description: Deduction from equality to equivalence of equalities.

Hypothesis

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

Assertion

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

Proof of Theorem cleq1d

Step	Hyp	Ref	Expression
1		cleq1d.1	. 2 ⊢ (φ → A = B)
2		cleq1 1107	. 2 ⊢ (A = B → (A = C ↔ B = C))
3	1, 2	syl 12	1 ⊢ (φ → (A = C ↔ B = C))

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

This theorem is referenced by:  cleq12d 1115  preq12b 1874  opprc3 1908  opth2 1909  frc 2172  frirr 2176  fr2nr 2177  fr3nr 2178  wefrc 2195  onfr 2237  nsuceq0 2306  fneq1 2718  fnun 2730  fnresdisj 2732  foeq1 2784  f1oco 2816  fvprc 2829  fveq1 2831  fveq2 2832  fvres 2840  funbrfv 2852  fnfvbr 2855  fvopabn 2873  elrnopab 2884  fconstfv 2903  f1fvf 2917  f1fveq 2918  isofrlem 2939  tz7.48lem 2993  tz7.49 2997  abianfplem 2999  elrnoprab 3054  caoprcan 3069  caoprmo 3084  om0r 3142  oe1m 3147  oawordeulem 3156  oawordeu 3157  nnmord 3189  erth 3219  map0 3268  mapsn 3269  endisj 3341  pw2en 3348  mapenlem2 3385  opthreg 3455  inf3lem2 3465  cplem2 3546  aceq5 3563  ac6lem 3575  kmlem8 3587  kmlem11 3590  zornlem6 3608  zornlem7 3609  fodomb 3615  unxpdomlem 3649  addnidpi 3822  ltexpi 3823  recmulpq 3864  dmrecpq 3868  ltexpq 3874  halfpq 3876  ltbtwnpq 3878  ltexpri 3943  recexpr 3954  00sr 4002  negexsr 4005  recexsrlem 4006  recexsr 4010  elreal 4044  axnegex 4078  axrecex 4079  axrnegex 4080  axrrecex 4081  addcan 4120  addcant 4122  negeu 4124  subval 4134  subadd 4143  subaddt 4145  subidt 4159  negcon1t 4167  subeq0t 4169  mulzer1t 4188  mulcan 4207  mulcant 4208  mul0ort 4212  receu 4215  divval 4217  divmul 4218  divmulz 4219  divmult 4220  divcan1z 4226  divcan2z 4227  divcan1t 4228  divcan2t 4229  divneq0bt 4230  recidt 4235  divcan3z 4249  divcan3t 4251  dividt 4256  rec11 4262  redivcl 4274  add20 4329  divge0 4392  nndiv 4453  crut 4531  0expt 4680  1expt 4681  sqe11t 4705  nn0opth2t 4726  sqr00t 4770  sqr2irrlem2 4778  sqr2irrlem3 4779  sqr2irrlem5 4781  replimt 4798  ruclem37 4921  infxpidmlem11 4943  hvsubeq0t 5040  hvsubaddt 5042  his6 5057  hial0 5058  hi2eqt 5059  orthcom 5061  normlem7t 5072  normsub0t 5085  normpytht 5092  ocelt 5162  ocsh 5164  ocorth 5172  ocin 5177  occllem5 5184  occllem8 5187  pjthlem14 5238  omls 5251  pjoc1t 5270  pjoc2t 5274  choc0 5291  chlejb1t 5429  chlejb2t 5430  h1deot 5454  h1de2 5458  pjoml5 5498  pjoml3t 5517  pjcht 5582  hods 5606  stelt 5671  stadd3 5689  strlem1 5691  str 5698  large 5700  golem2 5705  stcltr1 5707  sumdmdi 5785

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