Theorem eqeq1d 1483

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 1481	. 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 956

This theorem is referenced by:  eqeq12d 1489  sbceq2dig 2016  csbieb 2030  uniiunlem 2132  preq12b 2483  iin0 2740  opthgg 2789  opprc3 2797  opth2 2800  opeqsn 2802  frc 2920  frirr 2924  wefrc 2943  onfr 2986  nsuceq0 3053  fneq1 3582  fnun 3594  fnresdisj 3597  funimadisj 3606  foeq1 3668  foco 3682  fvprc 3721  fveq1 3723  fveq2 3724  fvres 3734  funbrfv 3750  fnbrfvb 3753  fvopabn 3786  elrnopabg 3800  dffo3 3819  fconstfv 3849  f1fvf 3875  f1fveq 3876  f1ocnvfv3 3883  isofrlem 3901  tz7.48lem 3955  tz7.49 3959  abianfplem 3961  caoprcan 4055  caoprmo 4070  op2ndg 4088  2ndconst 4097  elrnoprabg 4124  oe0m1 4160  om0r 4174  oe1m 4179  oawordeulem 4188  oawordeu 4189  omord 4199  oneo 4212  nneob 4255  erth 4282  mapsn 4345  endisj 4437  pw2en 4446  mapenlem2 4490  fodomfibOLD 4567  pm54.43 4572  opthreg 4604  aceq5 4740  kmlem9 4773  zorn2lem7 4794  fodomb 4800  unxpdomlem 4843  cfeq0 4914  addnidpi 5028  ltexpi 5029  recmulpq 5070  dmrecpq 5074  ltexpq 5080  halfpq 5082  ltbtwnpq 5084  ltexpri 5149  recexpr 5160  00sr 5208  negexsr 5211  recexsrlem 5212  recexsr 5216  elreal 5250  axrnegex 5283  axrrecex 5284  cnegextlem1 5345  cnegext 5348  addcan 5351  addcant 5352  negeu 5355  subvalt 5357  subadd 5371  subaddt 5375  subsub23t 5376  subidt 5395  neg11t 5409  negcon1t 5410  mul01t 5443  add20 5602  recext 5684  mulcan 5686  mulcanOLD 5687  mulcant2 5688  mulcant2OLD 5689  mul0ort 5696  muleqaddt 5700  receu 5701  divval 5704  divmul 5705  divmulz 5706  divmult 5707  divcan1z 5718  divcan2z 5719  divcan1t 5724  divcan1tOLD 5725  divcan2tOLD 5727  divne0bt 5728  recidt 5735  divcan3z 5754  divcan3t 5760  divcan3tOLD 5761  div11t 5765  rec11 5778  rec11rt 5779  redivcl 5798  nndivt 5959  flbit 6240  ioo0t 6368  icoun 6413  1expt 6584  expeq0t 6585  sq11t 6629  sqeqort 6649  nn0opth2t 6668  sqr00t 6714  sqr2irrlem2 6725  sqr2irrlem3 6726  sqr2irrlem5 6728  crut 6738  replimt 6761  abs00t 6853  abs1m 6904  climconst3 7096  ivthlem9 7289  isupivth 7290  dsupivthlem 7291  efcltlem2 7305  ef0lem 7310  reef11t 7409  reeff1olem1 7424  reeff1o 7426  acdc3 7487  acdc5 7493  unbenlem 7504  ruclem37 7546  infxpidmlem11 7562  retopbas 7655  0ntr 7702  ntreq0 7708  cldlp 7750  ismet 7798  ismsg 7800  msflem 7803  meteq0 7812  metreslem 7822  metxp 7834  methausi 7881  cnmet 7904  blssioo 7913  dscmet 7918  bcthlem33 8031  bcth 8032  isgrp 8041  isgrpi 8042  grpidinvlem3 8050  grpideu 8053  grpidval 8058  grpidinv2 8060  grpinveu 8064  grpinvval 8067  grpinv 8069  isgrp2i 8076  cnid 8127  addinv 8128  mulid 8132  ghgrpilem3 8135  isring 8141  ringi 8142  cnring 8162  ringsn 8163  vci 8167  isvclem 8196  isnvlem 8229  nvi 8233  nvmul0or 8272  nvsubadd 8275  nvsubsub23 8282  nvz 8297  imsmetlem 8323  iporthcom 8369  ipz 8372  lnoval 8413  nmorepnf 8431  nmlno0i 8454  nmlno0 8455  ajfval 8469  hmoval 8470  isphg 8476  isph 8481  ip2eqi 8517  minveceu 8583  minvecdist 8585  pilem1 8671  pilem2 8672  pilem3 8673  pilem4 8674  sinperlem2 8687  cosh111t 8717  efif 8721  efifolem3 8724  efifolem6 8727  efifolem7 8728  efifo 8729  efif1lem6 8735  efielcirc 8739  circgrp 8740  effoi 8745  logeftb 8764  hvmul0ort 8894  hvsubeq0t 8935  hvaddeq0t 8936  hvaddcant 8937  hvmulcant 8939  hvmulcan2t 8940  hvsubaddt 8944  his6t 8965  hial0 8968  hial02 8969  hi2eqt 8971  orthcom 8974  normlem7tALT 8985  normsub0t 9003  normpytht 9012  hilid 9028  norm1ex 9122  hhssnv 9134  ocelt 9154  ocsh 9156  ocorth 9164  ocin 9169  occllem5 9177  occllem8 9180  pjthlem13 9231  pjthlem14 9232  pjeq2t 9241  omls 9246  pjoc1t 9267  pjomlt 9269  pjoc2t 9272  choc0 9290  chm0t 9414  chocint 9418  chlejb1t 9435  chlejb2t 9436  chjot 9438  h1deot 9472  h1de2 9476  pjoml6 9532  pjoml2t 9554  pjoml3t 9555  pjcht 9639  pj11t 9659  hods 9701  hodidt 9718  eigortht 9764  nmoprepnf 9794  elunopt 9799  nmfnrepnf 9807  nlfnvalt 9808  adjvalt 9814  eigvecvalt 9822  unopf1ot 9840  elnlfnt 9852  adjt 9857  adjeqt 9859  hmdmadjt 9864  nmlnop0t 9923  lnopeq0 9932  lnopeq 9933  lnopeqt 9934  elunop2t 9938  lnfn0t 9976  riesz4 9996  riesz4t 9997  riesz1t 9998  cnlnadjlem3 10002  cnlnadjlem4 10003  cnlnadjlem5 10004  cnlnadjeut 10011  cnlnssadj 10013  adjbd1o 10018  nmopadjle 10021  hmopidmcht 10081  hmopidmpjt 10082  pjima 10104  pjhmopidm 10110  stelt 10141  hstelt 10142  hstel2t 10146  stadd3 10175  strlem1 10177  str 10184  hstr 10192  large 10194  golem2 10199  stcltr1 10201  superpos 10281  sumdmdi 10342  mddmdin0 10358  elghomlem1 10382  ghomgsg 10395  ghomf1olem 10396  cayleylem3 10411  erdisj2 10442  hmeogrp 10538  eqindhome 10541  rcfpfillem6 10595  rcfpfillem6OLD 10596  dtt2 10618  isded 10669  dedi 10670  cmppfd 10678  domcmpd 10679  codcmpd 10680  iscat 10687  cati 10688  cmpasso 10706  cmpida 10707  cmpidb 10708  ishoma 10715  ishomc 10717  ishomd 10718  ismonb2 10740  cmpmon 10743  isepib2 10750  isfuna 10754  isfunb 10755  ishgrag 10769  hgralem 10770  ispgrag 10779

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain