Theorem eqeq1d 1480

Description: Deduction from equality to equivalence of equalities.

Hypothesis

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

Assertion

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

Proof of Theorem eqeq1d

Step	Hyp	Ref	Expression
1		eqeq1d.1	. 2 |- (ph -> A = B)
2		eqeq1 1478	. 2 |- (A = B -> (A = C <-> B = C))
3	1, 2	syl 10	1 |- (ph -> (A = C <-> B = C))

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

This theorem is referenced by:  eqeq12d 1486  sbceq2dig 2012  csbieb 2026  uniiunlem 2128  preq12b 2479  iin0 2735  opthgg 2784  opprc3 2792  opth2 2795  opeqsn 2797  frc 2915  frirr 2919  wefrc 2938  onfr 2981  nsuceq0 3048  fneq1 3574  fnun 3586  fnresdisj 3589  funimadisj 3598  foeq1 3659  foco 3673  fvprc 3712  fveq1 3714  fveq2 3715  fvres 3725  funbrfv 3741  fnbrfvb 3744  fvopabn 3777  elrnopabg 3791  dffo3 3810  fconstfv 3840  f1fvf 3866  f1fveq 3867  f1ocnvfv3 3874  isofrlem 3892  tz7.48lem 3946  tz7.49 3950  abianfplem 3952  caoprcan 4047  caoprmo 4062  op2ndg 4078  2ndconst 4087  elrnoprabg 4114  oe0m1 4150  om0r 4164  oe1m 4169  oawordeulem 4178  oawordeu 4179  omord 4189  oneo 4202  nneob 4245  erth 4272  mapsn 4335  endisj 4423  pw2en 4432  mapenlem2 4476  fodomfib 4547  pm54.43 4552  opthreg 4584  aceq5 4720  kmlem9 4753  zorn2lem7 4774  fodomb 4780  unxpdomlem 4823  cfeq0 4894  addnidpi 5008  ltexpi 5009  recmulpq 5050  dmrecpq 5054  ltexpq 5060  halfpq 5062  ltbtwnpq 5064  ltexpri 5129  recexpr 5140  00sr 5188  negexsr 5191  recexsrlem 5192  recexsr 5196  elreal 5230  axrnegex 5263  axrrecex 5264  cnegextlem1 5325  cnegext 5328  addcan 5331  addcant 5332  negeu 5335  subvalt 5337  subadd 5351  subaddt 5355  subsub23t 5356  subidt 5375  neg11t 5389  negcon1t 5390  mul01t 5423  add20 5584  recext 5665  mulcan 5667  mulcant2 5668  mul0ort 5673  muleqaddt 5677  receu 5678  divval 5681  divmul 5682  divmulz 5683  divmult 5684  divcan1z 5695  divcan2z 5696  divcan1t 5697  divcan2t 5698  divne0bt 5699  recidt 5706  divcan3z 5724  divcan3t 5726  div11t 5729  rec11 5742  rec11rt 5743  redivcl 5762  nndivt 5914  flbit 6192  ioo0t 6313  icoun 6354  1expt 6524  expeq0t 6525  sq0t 6558  sq11t 6568  sqeqort 6588  nn0opth2t 6606  sqr00t 6652  sqr2irrlem2 6663  sqr2irrlem3 6664  sqr2irrlem5 6666  crut 6676  replimt 6700  abs00t 6796  abs1m 6849  climconst3 7041  ivthlem9 7232  isupivth 7233  dsupivthlem 7234  efcltlem2 7255  ef0lem 7260  reeff1 7358  reeff1olem1 7372  reeff1olem1OLD 7374  reeff1o 7376  acdc3 7437  acdc5 7443  unbenlem 7455  ruclem37 7497  infxpidmlem11 7513  retopbas 7605  0ntr 7652  ntreq0 7658  cldlp 7700  ismet 7748  ismsg 7750  msflem 7753  meteq0 7762  metreslem 7774  metxp 7786  methausi 7833  cnmet 7856  blssioo 7865  dscmet 7870  bcthlem33 7981  bcth 7982  isgrp 7991  isgrpi 7992  grpidinvlem3 8000  grpideu 8003  grpidval 8008  grpidinv2 8010  grpinveu 8014  grpinvval 8017  grpinv 8019  isgrp2i 8026  cnid 8079  addinv 8080  mulid 8084  ghgrpilem3 8087  isring 8093  ringi 8094  cnring 8114  ringsn 8115  vci 8119  isvclem 8148  isnvlem 8181  nvi 8185  nvmul0or 8224  nvsubadd 8227  nvsubsub23 8234  nvz 8249  imsmetlem 8274  iporthcom 8316  ipz 8319  lnoval 8360  nmorepnf 8376  nmlno0i 8399  nmlno0 8400  ajfval 8413  hmoval 8414  isphg 8420  isph 8425  ip2eqi 8461  minveceu 8527  minvecdist 8529  pilem1 8609  pilem2 8610  pilem3 8611  pilem4 8612  sinperlem2 8625  cosh111t 8651  efif 8655  efifolem3 8658  efifolem6 8661  efifolem7 8662  efifo 8663  efif1lem6 8669  elcircOLD 8673  efielcirc 8678  circgrp 8679  effoi 8684  logeftb 8703  hvmul0ort 8833  hvsubeq0t 8874  hvaddeq0t 8875  hvaddcant 8876  hvmulcant 8878  hvmulcan2t 8879  hvsubaddt 8883  his6t 8904  hial0 8907  hial02 8908  hi2eqt 8910  orthcom 8913  normlem7tALT 8924  normsub0t 8942  normpytht 8951  hilid 8967  norm1ex 9061  hhssnv 9073  ocelt 9093  ocsh 9095  ocorth 9103  ocin 9108  occllem5 9116  occllem8 9119  pjthlem13 9169  pjthlem14 9170  pjeq2t 9179  omls 9184  pjoc1t 9205  pjomlt 9207  pjoc2t 9210  choc0 9228  chm0t 9352  chocint 9356  chlejb1t 9373  chlejb2t 9374  chjot 9376  h1deot 9410  h1de2 9414  pjoml6 9472  pjoml2t 9494  pjoml3t 9495  pjcht 9579  pj11t 9599  hods 9641  hodidt 9658  eigortht 9704  nmoprepnf 9734  elunopt 9739  nmfnrepnf 9747  nlfnvalt 9748  adjvalt 9754  eigvecvalt 9762  unopf1ot 9779  elnlfnt 9791  adjt 9796  adjeqt 9798  hmdmadjt 9803  nmlnop0t 9861  lnopeq0 9870  lnopeq 9871  lnopeqt 9872  elunop2t 9876  lnfn0t 9914  riesz4 9934  riesz4t 9935  riesz1t 9936  cnlnadjlem3 9940  cnlnadjlem4 9941  cnlnadjlem5 9942  cnlnadjeut 9949  cnlnssadj 9951  adjbd1o 9956  nmopadjle 9959  hmopidmcht 10019  hmopidmpjt 10020  pjima 10042  pjhmopidm 10048  stelt 10079  hstelt 10080  hstel2t 10084  stadd3 10113  strlem1 10115  str 10122  hstr 10130  large 10132  golem2 10137  stcltr1 10139  superpos 10218  sumdmdi 10278  mddmdin0 10292  elghomlem1 10316  ghomgsg 10329  ghomf1olem 10330  cayleylem3 10345  erdisj2 10379  hmeogrp 10461  dtt2 10498  isded 10549  dedi 10550  cmppfd 10558  domcmpd 10559  codcmpd 10560  iscat 10567  cati 10568  cmpasso 10586  cmpida 10587  cmpidb 10588  ishoma 10595  ishomc 10597  ishomd 10598  ismonb2 10618  cmpmon 10621  isfuna 10628  isfunb 10629  ishgrag 10641  hgralem 10642  ispgrag 10651

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

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

Copyright terms: Public domain