Theorem eqeq2d 1478

Description: Deduction from equality to equivalence of equalities.

Hypothesis

Ref	Expression
eqeq2d.1	|- (ph -> A = B)

Assertion

Ref	Expression
eqeq2d	|- (ph -> (C = A <-> C = B))

Proof of Theorem eqeq2d

Step	Hyp	Ref	Expression
1		eqeq2d.1	. 2 |- (ph -> A = B)
2		eqeq2 1476	. 2 |- (A = B -> (C = A <-> C = B))
3	1, 2	syl 10	1 |- (ph -> (C = A <-> C = B))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953

This theorem is referenced by:  eqeq12d 1481  eqtrd 1499  eq2tr 1525  sbceq1dig 2004  eusn 2436  cbvopab 2662  cbvopab1 2664  cbvopab1s 2665  cbvopab2v 2667  opthg 2778  eqvinop 2781  moop2 2790  opabid 2799  dfid3 2826  reusn 2882  reusni 2883  limeq 2950  onsucuni2 3081  onuninsuc 3098  relop 3265  elxp4 3439  elxp5 3440  funopg 3533  funcnvuni 3550  fnopabfv 3743  ssimaex 3753  fvopab4g 3764  fvopabn 3771  fopabap 3826  fconst5 3833  abrexexlem1 3843  abrexexlem2 3844  abrexex 3845  f1fvf 3860  f1fveq 3861  f1ocnvfv 3865  f1ocnvfvb 3866  tz7.44-2 3914  tz7.44-3 3915  rdgeq1 3919  rdgeq2 3920  rdglem2 3923  tz7.48lem 3940  rcla4eopr 3975  dfoprab2 3976  cbvoprab12 3983  fnoprval 4002  oprabval2gf 4011  oprabval3 4015  oprabval4g 4016  oprabval6g 4017  fnrnoprval 4021  fooprval 4022  oprvalex 4026  caoprcan 4041  fo1st 4075  fo2nd 4076  2ndconst 4081  dfoprab5 4099  omv 4135  oev 4137  oe1m 4163  oarec 4180  nneob 4239  qseq2 4273  ecelqsi 4276  snec 4280  ecoptocl 4287  th3qlem1 4298  th3qlem2 4299  th3q 4301  en1 4407  mapsnen 4410  xpsnen 4415  xpassen 4421  pw2en 4426  mapxpen 4475  xpmapenlem3 4478  xpmapenlem4 4479  xpmapenlem5 4480  mapunen 4482  unfilem3 4526  abfii2 4536  abfii3 4537  abfii4 4538  pwfilem 4544  tz9.12lem1 4631  tz9.12lem3 4633  rankr1g 4647  rankuni 4670  aceq3lem 4704  aceq5lem1 4707  aceq5lem4 4710  aceq6b 4714  kmlem9 4745  unidom 4780  oncard 4801  cardsn 4806  cardalephex 4858  cf0 4882  cflecard 4884  cfsuc 4887  indpi 5006  genpv 5074  genpprecl 5076  genpass 5084  distrlem1pr 5099  distrlem5pr 5103  1idpr 5105  axcnre 5258  addcant 5324  subeq0t 5375  neg11t 5381  mulcant2 5660  divmul3t 5678  div11t 5721  diveq0t 5724  rec11 5734  negeq0t 5762  infm3lem 6000  nn0ind-raph 6162  zqt 6198  qnegclt 6208  seq1lem1 6246  seq1val 6249  seq1suclem 6253  shftfval 6279  2shft 6289  dfioo2 6336  icoshftf1oi 6342  icoshftf1olem 6343  limsupvalt 6461  expge0t 6522  expge1t 6524  sq11t 6560  sqeqort 6580  nn0opth2t 6598  sqrmsq2 6636  sqr2irrlem2 6655  sqr2irrlem3 6656  sqr2irrlem5 6658  cru 6667  crut 6668  creur 6673  creui 6674  replimt 6692  abssubne0t 6820  abs1m 6841  sumeq2 6923  cbvsum 6924  serzfsum 6942  fsumsplit 6958  serzclim0 7046  climaddc2 7055  climmulc2 7065  infcvgaux1 7154  infcvgaux2 7155  geolim 7172  geolim1 7174  divccncf 7215  efseq1ex 7248  eftlext 7320  ef1tlub 7324  ef01tlub 7327  absef01tlub 7329  eirr 7335  ef4pt 7341  reeff1 7350  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  nn0ennn 7439  znnenlemOLD 7444  ruclem12 7464  eltopsp 7546  tpsex 7547  istps 7548  tgval3t 7567  subbas 7586  subbas2 7587  subtop 7588  ntrfval 7609  clsfval 7610  neifval 7655  lpfval 7683  islp2 7688  qdensere 7691  cnpfval 7697  blfval 7775  blrn3 7787  blelrn 7788  metdnsconst 7840  metcn4i 7906  xplm 7909  opr1cn 7912  opr2cn 7913  opr1scn 7914  fsumcnlem 7923  bcth 7966  isgrp 7975  grpid 7999  grpinvfval 8000  grpinvf 8014  grpdivfval 8016  grplactfval 8032  grplactf1o 8034  vci 8104  isvcgOLD 8133  isvclem 8134  isnvlem 8167  isnvgOLD 8168  nvi 8173  nvmfval 8204  cnnvm 8251  ipfval 8286  ip1cnilem4 8310  ip1cnilem5 8311  ip1cnilem6 8312  lnoval 8347  nmofval 8357  nmoval 8358  nmosetn0 8360  nmolb 8366  nmo0 8383  nmlno0lem 8385  nmlno0 8387  ajfval 8400  ipasslem6 8426  ipasslem11 8431  siilem2 8443  ajmoi 8450  minvecex 8509  htthlem3 8552  htthlem5 8554  spwval2 8577  spwval 8582  cosh111t 8632  efghgrpilem 8634  efifolem1 8637  efifolem2 8638  efifolem3 8639  efifolem6 8642  efifo 8644  efif1lem6 8650  eff1i 8665  effoi 8666  effoiOLD 8667  hvaddcant 8858  hiret 8881  hilnorm 8951  projlem8 9109  projlem10 9111  projlem15 9116  pjtheu 9150  pjmvalt 9153  pjeq2t 9156  omlsi 9160  pjtheu2 9165  pjpj0 9170  axpjpjt 9171  shsel3t 9194  shscomt 9198  dfchsup2 9213  dfchj2 9239  dfchj3 9240  h1de2ctlem 9394  elspansnt 9405  elspansn2t 9406  spansncol 9407  spanunsn 9419  h1datomt 9422  hosmvalt 9428  hommvalt 9429  hodmvalt 9430  hfsmvalt 9431  hfmmvalt 9432  cmbrt 9444  osumlem5 9499  spansncv 9514  spansncvt 9515  pjrn 9564  pj11t 9576  pjpytht 9587  ho01 9671  adjmo 9675  eigret 9678  eigortht 9681  nmopvalt 9699  nmopsetn0 9709  nmfnvalt 9720  nmfnsetn0 9722  eigvalvalt 9740  nmoplbt 9748  nmfnlbt 9764  adjt 9773  adjeqt 9775  adjvalvalt 9777  bravalt 9783  bra0 9790  brafnmult 9791  kbvalt 9792  kbmult 9795  eighmortht 9804  nmopneg 9805  nmop0 9826  nmfn0 9827  nmlnop0ALT 9835  lnopeqt 9849  nmopunt 9854  lnopcon 9878  lnfncon 9905  riesz3 9910  riesz4 9911  cnlnadjlem5 9919  cnlnadjlem9 9923  cnlnadj 9924  cnlnssadj 9928  nmopadjle 9936  branmfnt 9951  rnbra 9953  cnvbravalt 9956  kbass2t 9962  kbass5t 9965  elpjrncht 10028  atom1d 10188  superpos 10189  sumdmdlem 10252  cdjreu 10264  cdj3lem2 10267  cdj3lem3 10270  cdj3lem3b 10272  elghomlem1 10287  ghomf1olem 10301  cayleylem2 10317  infi1 10347  fine 10348  abfi 10349  ficli 10368  bsi 10382  hmeogrp 10425  subsp 10429  infi 10448  cnfilca 10451  trran 10480  trnij 10481  cnvtr 10482  isded 10513  dedi 10514  cmppfd 10522  domcmpd 10523  codcmpd 10524  iscat 10531  cati 10532  cmpasso 10550  ishoma 10559  ishomb 10560  ismonb 10580  ismonb2 10582  cmpmon 10585

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

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

Copyright terms: Public domain