Theorem eqeq1d 1486

Description: Deduction from equality to equivalence of equalities.

Hypothesis

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

Assertion

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

Proof of Theorem eqeq1d

Step	Hyp	Ref	Expression
1		eqeq1d.1	. 2 ⊢ (φ → A = B)
2		eqeq1 1484	. 2 ⊢ (A = B → (A = C ↔ B = C))
3	1, 2	syl 10	1 ⊢ (φ → (A = C ↔ B = C))

Syntax hints:   → wi 3   ↔ wb 146   = wceq 958

This theorem is referenced by:  eqeq12d 1492  sbceq2dig 2019  csbieb 2033  uniiunlem 2135  preq12b 2487  iin0 2745  opthgg 2795  opprc3 2803  opth2 2806  opeqsn 2808  frc 2926  frirr 2930  wefrc 2949  onfr 2992  nsuceq0 3059  fneq1 3588  fnun 3600  fnresdisj 3603  funimadisj 3612  foeq1 3674  foco 3688  fvprc 3727  fveq1 3729  fveq2 3730  fvres 3740  funbrfv 3756  fnbrfvb 3759  fvopabn 3792  elrnopabg 3806  dffo3 3825  fconstfv 3855  f1fvf 3881  f1fveq 3882  f1ocnvfv3 3889  isofrlem 3907  tz7.48lem 3961  tz7.49 3965  abianfplem 3967  caoprcan 4061  caoprmo 4076  op2ndg 4094  2ndconst 4103  elrnoprabg 4130  oe0m1 4166  om0r 4180  oe1m 4185  oawordeulem 4194  oawordeu 4195  omord 4205  oneo 4218  nneob 4261  erth 4288  mapsn 4351  endisj 4443  pw2en 4452  mapenlem2 4496  pm54.43 4581  opthreg 4613  aceq5 4750  kmlem9 4783  zorn2lem7 4804  fodomb 4810  unxpdomlem 4854  cfeq0 4926  addnidpi 5040  ltexpi 5041  recmulpq 5082  dmrecpq 5086  ltexpq 5092  halfpq 5094  ltbtwnpq 5096  ltexpri 5161  recexpr 5172  00sr 5220  negexsr 5223  recexsrlem 5224  recexsr 5228  elreal 5262  axrnegex 5295  axrrecex 5296  cnegextlem1 5357  cnegext 5360  addcan 5363  addcant 5364  negeu 5367  subvalt 5369  subadd 5383  subaddt 5387  subsub23t 5388  subidt 5407  neg11t 5421  negcon1t 5422  mul01t 5455  add20 5614  recext 5696  mulcan 5698  mulcanOLD 5699  mulcant2 5700  mulcant2OLD 5701  mul0ort 5708  muleqaddt 5712  receu 5713  divval 5716  divmul 5717  divmulz 5718  divmult 5719  divcan1z 5730  divcan2z 5731  divcan1t 5732  divcan2tOLD 5734  divne0bt 5735  recidt 5742  divcan3z 5761  divcan3t 5763  div11t 5766  rec11 5780  rec11rt 5781  redivcl 5800  nndivt 5961  flbit 6242  ioo0t 6369  icoun 6414  1expt 6585  expeq0t 6586  sq11t 6630  sqeqort 6650  nn0opth2t 6669  sqr00t 6715  sqr2irrlem2 6726  sqr2irrlem3 6727  sqr2irrlem5 6729  crut 6739  replimt 6762  abs00t 6853  abs1m 6904  climconst3 7096  ivthlem9 7289  isupivth 7290  dsupivthlem 7291  efcltlem2 7305  ef0lem 7310  reef11t 7409  reeff1olem1 7424  reeff1o 7426  acdc3 7488  acdc5 7494  unbenlem 7505  ruclem37 7547  infxpidmlem11 7563  retopbas 7652  0ntr 7699  ntreq0 7705  cldlp 7747  ismet 7795  ismsg 7797  msflem 7800  meteq0 7809  metreslem 7819  metxp 7831  methausi 7878  cnmet 7901  blssioo 7910  dscmet 7915  bcthlem33 8028  bcth 8029  isgrp 8038  isgrpi 8039  grpidinvlem3 8047  grpideu 8050  grpidval 8054  grpidinv2 8056  grpinveu 8060  grpinvval 8063  grpinv 8065  isgrp2i 8072  cnid 8123  addinv 8124  mulid 8128  ghgrpilem3 8131  isring 8137  ringi 8138  cnring 8158  ringsn 8159  vci 8163  isvclem 8192  isnvlem 8225  nvi 8229  nvmul0or 8268  nvsubadd 8271  nvsubsub23 8278  nvz 8293  imsmetlem 8319  iporthcom 8365  ipz 8368  lnoval 8409  nmorepnf 8427  nmlno0i 8450  nmlno0 8451  ajfval 8465  hmoval 8466  isphg 8472  isph 8477  ip2eqi 8513  minveceu 8579  minvecdist 8581  pilem1 8666  pilem2 8667  pilem3 8668  pilem4 8669  sinperlem2 8682  cosh111t 8712  efif 8716  efifolem3 8719  efifolem6 8722  efifolem7 8723  efifo 8724  efif1lem6 8730  efielcirc 8734  circgrp 8735  effoi 8740  logeftb 8759  hvmul0ort 8889  hvsubeq0t 8930  hvaddeq0t 8931  hvaddcant 8932  hvmulcant 8934  hvmulcan2t 8935  hvsubaddt 8939  his6t 8960  hial0 8963  hial02 8964  hi2eqt 8966  orthcom 8969  normlem7tALT 8980  normsub0t 8998  normpytht 9007  hilid 9023  norm1ex 9117  hhssnv 9129  ocelt 9149  ocsh 9151  ocorth 9159  ocin 9164  occllem5 9172  occllem8 9175  pjthlem13 9226  pjthlem14 9227  pjeq2t 9236  omls 9241  pjoc1t 9262  pjomlt 9264  pjoc2t 9267  choc0 9285  chm0t 9409  chocint 9413  chlejb1t 9430  chlejb2t 9431  chjot 9433  h1deot 9467  h1de2 9471  pjoml6 9527  pjoml2t 9549  pjoml3t 9550  pjcht 9634  pj11t 9654  hods 9696  hodidt 9713  eigortht 9759  nmoprepnf 9789  elunopt 9794  nmfnrepnf 9802  nlfnvalt 9803  adjvalt 9809  eigvecvalt 9817  unopf1ot 9835  elnlfnt 9847  adjt 9852  adjeqt 9854  hmdmadjt 9859  nmlnop0t 9918  lnopeq0 9927  lnopeq 9928  lnopeqt 9929  elunop2t 9933  lnfn0t 9971  riesz4 9991  riesz4t 9992  riesz1t 9993  cnlnadjlem3 9997  cnlnadjlem4 9998  cnlnadjlem5 9999  cnlnadjeut 10006  cnlnssadj 10008  adjbd1o 10013  nmopadjle 10016  hmopidmcht 10076  hmopidmpjt 10077  pjima 10099  pjhmopidm 10105  stelt 10136  hstelt 10137  hstel2t 10141  stadd3 10170  strlem1 10172  str 10179  hstr 10187  large 10189  golem2 10194  stcltr1 10196  superpos 10276  sumdmdi 10337  mddmdin0 10353  elghomlem1 10377  ghomgsg 10390  ghomf1olem 10391  cayleylem3 10406  erdisj2 10437  hmeogrp 10524  eqindhome 10527  rcfpfillem6 10568  dtt2 10589  isded 10640  dedi 10641  cmppfd 10649  domcmpd 10650  codcmpd 10651  iscat 10658  cati 10659  cmpasso 10677  cmpida 10678  cmpidb 10679  ishoma 10686  ishomc 10688  ishomd 10689  ismonb2 10711  cmpmon 10714  isepib2 10721  isfuna 10725  isfunb 10726  ishgrag 10740  hgralem 10741  ispgrag 10750

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1472

Copyright terms: Public domain