Theorem eqeq2d 1484

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 1482	. 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 955

This theorem is referenced by:  eqeq12d 1487  eqtrd 1505  eq2tr 1531  sbceq1dig 2011  eusn 2443  cbvopab 2668  cbvopab1 2670  cbvopab1s 2671  cbvopab2v 2673  opthg 2784  eqvinop 2787  moop2 2797  opabid 2806  dfid3 2832  reusn 2888  reusni 2889  limeq 2956  onsucuni2 3087  onuninsuc 3104  relop 3271  elxp4 3449  elxp5 3450  funopg 3543  funcnvuni 3560  fnopabfv 3753  ssimaex 3763  fvopab4g 3774  fvopabn 3781  fopabap 3836  fconst5 3843  abrexexlem1 3853  abrexexlem2 3854  abrexex 3855  f1fvf 3870  f1fveq 3871  f1ocnvfv 3875  f1ocnvfvb 3876  tz7.44-2 3924  tz7.44-3 3925  rdgeq1 3929  rdgeq2 3930  rdglem2 3933  tz7.48lem 3950  rcla4eopr 3985  dfoprab2 3986  cbvoprab12 3993  fnoprval 4012  oprabval2gf 4021  oprabval3 4025  oprabval4g 4026  oprabval6g 4027  fnrnoprval 4031  fooprval 4032  oprvalex 4036  caoprcan 4050  fo1st 4084  fo2nd 4085  2ndconst 4090  dfoprab5 4108  omv 4144  oev 4146  oe1m 4172  oarec 4189  nneob 4248  qseq2 4282  ecelqsi 4285  snec 4289  ecoptocl 4296  th3qlem1 4307  th3qlem2 4308  th3q 4310  en1 4416  mapsnen 4419  xpsnen 4424  xpassen 4430  pw2en 4435  mapxpen 4484  xpmapenlem3 4487  xpmapenlem4 4488  xpmapenlem5 4489  mapunen 4491  unfilem3 4535  abfii2 4545  abfii3 4546  abfii4 4547  pwfilem 4553  tz9.12lem1 4642  tz9.12lem3 4644  rankr1g 4658  rankuni 4681  aceq3lem 4715  aceq5lem1 4718  aceq5lem4 4721  aceq6b 4725  kmlem9 4756  unidom 4791  oncard 4812  cardsn 4817  cardalephex 4869  cf0 4893  cflecard 4895  cfsuc 4898  indpi 5017  genpv 5085  genpprecl 5087  genpass 5095  distrlem1pr 5110  distrlem5pr 5114  1idpr 5116  axcnre 5269  addcant 5335  subeq0t 5386  neg11t 5392  mulcant2 5670  divmul3t 5688  div11t 5731  diveq0t 5734  rec11 5744  negeq0t 5772  infm3lem 6010  nn0ind-raph 6172  zqt 6210  qnegclt 6220  seq1lem1 6259  seq1val 6262  seq1suclem 6266  shftfval 6292  2shft 6302  dfioo2 6349  icoshftf1oi 6355  icoshftf1olem 6356  limsupvalt 6474  expge0t 6536  expge1t 6538  sq11t 6574  sqeqort 6594  nn0opth2t 6613  sqrmsq2 6651  sqr2irrlem2 6670  sqr2irrlem3 6671  sqr2irrlem5 6673  cru 6682  crut 6683  creur 6688  creui 6689  replimt 6707  abssubne0t 6835  abs1m 6856  sumeq2 6938  cbvsum 6939  serzfsum 6957  fsumsplit 6973  serzclim0 7062  climaddc2 7072  climmulc2 7082  infcvgaux1 7171  infcvgaux2 7172  geolim 7189  geolim1 7191  divccncf 7232  efseq1ex 7265  eftlext 7337  ef1tlub 7341  ef01tlub 7344  absef01tlub 7346  eirr 7352  ef4pt 7358  reeff1 7367  acdc3 7446  acdc2 7449  acdc5 7452  acdc 7454  nn0ennn 7456  znnenlemOLD 7461  ruclem12 7481  eltopsp 7564  tpsex 7565  istps 7566  tgval3t 7585  subbas 7604  subbas2 7605  subtop 7606  ntrfval 7627  clsfval 7628  neifval 7674  lpfval 7702  islp2 7707  qdensere 7711  cnpfval 7717  blfval 7797  blrn3 7809  blelrn 7810  metdnsconst 7863  metcn4i 7934  xplm 7937  opr1cn 7940  opr2cn 7941  opr1scn 7942  fsumcnlem 7951  bcth 7994  isgrp 8003  grpid 8027  grpinvfval 8028  grpinvf 8041  grpdivfval 8043  grplactfval 8059  grplactf1o 8061  vci 8131  isvclem 8160  isnvlem 8193  nvi 8197  nvmfval 8228  nvdm 8253  cnnvm 8277  ipfval 8314  ip1cnilem4 8338  ip1cnilem5 8339  ip1cnilem6 8340  lnoval 8375  nmofval 8385  nmoval 8386  nmosetn0 8388  nmolb 8394  nmo0 8411  nmlno0lem 8413  nmlno0 8415  ajfval 8428  ipasslem6 8454  ipasslem11 8459  siilem2 8471  ajmoi 8478  minvecex 8537  htthlem3 8580  htthlem5 8582  spwval2 8610  spwval 8616  cosh111t 8667  efghgrpilem 8669  efifolem1 8672  efifolem2 8673  efifolem3 8674  efifolem6 8677  efifo 8679  efif1lem6 8685  eff1i 8699  effoi 8700  hvaddcant 8892  hiret 8915  hilnorm 8985  projlem8 9148  projlem10 9150  projlem15 9155  pjtheu 9190  pjmvalt 9193  pjeq2t 9196  omlsi 9200  pjtheu2 9205  pjpj0 9210  axpjpjt 9211  shsel3t 9234  shscomt 9238  dfchsup2 9253  dfchj2 9279  dfchj3 9280  h1de2ctlem 9434  elspansnt 9445  elspansn2t 9446  spansncol 9447  spanunsn 9459  h1datomt 9462  hosmvalt 9468  hommvalt 9469  hodmvalt 9470  hfsmvalt 9471  hfmmvalt 9472  cmbrt 9484  osumlem5 9539  spansncv 9554  spansncvt 9555  pjrn 9604  pj11t 9616  pjpytht 9627  ho01 9711  adjmo 9715  eigret 9718  eigortht 9721  nmopvalt 9739  nmopsetn0 9749  nmfnvalt 9760  nmfnsetn0 9762  eigvalvalt 9780  nmoplbt 9788  nmfnlbt 9805  adjt 9814  adjeqt 9816  adjvalvalt 9818  bravalt 9824  bra0 9831  brafnmult 9832  kbvalt 9833  kbmult 9836  eighmortht 9845  nmopneg 9846  nmop0 9867  nmfn0 9868  nmlnop0ALT 9876  lnopeqt 9890  nmopunt 9895  lnopcon 9919  lnfncon 9946  riesz3 9951  riesz4 9952  cnlnadjlem5 9960  cnlnadjlem9 9964  cnlnadj 9965  cnlnssadj 9969  nmopadjle 9977  branmfnt 9994  rnbra 9996  cnvbravalt 9999  kbass2t 10006  kbass5t 10009  elpjrncht 10074  atom1d 10236  superpos 10237  sumdmdlem 10301  cdjreu 10315  cdj3lem2 10318  cdj3lem3 10321  cdj3lem3b 10323  elghomlem1 10338  ghomf1olem 10352  cayleylem2 10366  infi1 10405  fine 10406  abfi 10407  ficli 10426  bsi 10441  hmeogrp 10484  subsp 10488  infi 10507  cnfilca 10510  rcfpfillem3 10513  rcfpfillem4 10514  rcfpfillem5 10515  rcfpfillem6 10516  sfvlim 10522  trran 10552  trnij 10553  cnvtr 10554  isded 10585  dedi 10586  cmppfd 10594  domcmpd 10595  codcmpd 10596  iscat 10603  cati 10604  cmpasso 10622  ishoma 10631  ishomb 10632  ismonb 10652  ismonb2 10654  cmpmon 10657  idfisf 10670

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

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

Copyright terms: Public domain