Theorem eqeq1d 1482

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

This theorem is referenced by:  eqeq12d 1488  sbceq2dig 2014  csbieb 2028  uniiunlem 2130  preq12b 2481  iin0 2737  opthgg 2786  opprc3 2794  opth2 2797  opeqsn 2799  frc 2917  frirr 2921  wefrc 2940  onfr 2983  nsuceq0 3050  fneq1 3579  fnun 3591  fnresdisj 3594  funimadisj 3603  foeq1 3665  foco 3679  fvprc 3718  fveq1 3720  fveq2 3721  fvres 3731  funbrfv 3747  fnbrfvb 3750  fvopabn 3783  elrnopabg 3797  dffo3 3816  fconstfv 3846  f1fvf 3872  f1fveq 3873  f1ocnvfv3 3880  isofrlem 3898  tz7.48lem 3952  tz7.49 3956  abianfplem 3958  caoprcan 4052  caoprmo 4067  op2ndg 4085  2ndconst 4094  elrnoprabg 4121  oe0m1 4157  om0r 4171  oe1m 4176  oawordeulem 4185  oawordeu 4186  omord 4196  oneo 4209  nneob 4252  erth 4279  mapsn 4342  endisj 4430  pw2en 4439  mapenlem2 4483  fodomfib 4554  pm54.43 4559  opthreg 4591  aceq5 4727  kmlem9 4760  zorn2lem7 4781  fodomb 4787  unxpdomlem 4830  cfeq0 4901  addnidpi 5015  ltexpi 5016  recmulpq 5057  dmrecpq 5061  ltexpq 5067  halfpq 5069  ltbtwnpq 5071  ltexpri 5136  recexpr 5147  00sr 5195  negexsr 5198  recexsrlem 5199  recexsr 5203  elreal 5237  axrnegex 5270  axrrecex 5271  cnegextlem1 5332  cnegext 5335  addcan 5338  addcant 5339  negeu 5342  subvalt 5344  subadd 5358  subaddt 5362  subsub23t 5363  subidt 5382  neg11t 5396  negcon1t 5397  mul01t 5430  add20 5590  recext 5671  mulcan 5673  mulcant2 5674  mul0ort 5679  muleqaddt 5683  receu 5684  divval 5687  divmul 5688  divmulz 5689  divmult 5690  divcan1z 5701  divcan2z 5702  divcan1t 5703  divcan2t 5704  divne0bt 5705  recidt 5712  divcan3z 5730  divcan3t 5732  div11t 5735  rec11 5748  rec11rt 5749  redivcl 5768  nndivt 5920  flbit 6201  ioo0t 6323  icoun 6364  1expt 6534  expeq0t 6535  sq11t 6579  sqeqort 6599  nn0opth2t 6619  sqr00t 6665  sqr2irrlem2 6676  sqr2irrlem3 6677  sqr2irrlem5 6679  crut 6689  replimt 6713  abs00t 6815  abs1m 6869  climconst3 7064  ivthlem9 7260  isupivth 7261  dsupivthlem 7262  efcltlem2 7283  ef0lem 7288  reeff1 7386  reeff1olem1 7400  reeff1olem1OLD 7402  reeff1o 7404  acdc3 7465  acdc5 7471  unbenlem 7483  ruclem37 7525  infxpidmlem11 7541  retopbas 7634  0ntr 7681  ntreq0 7687  cldlp 7729  ismet 7777  ismsg 7779  msflem 7782  meteq0 7791  metreslem 7803  metxp 7815  methausi 7864  cnmet 7887  blssioo 7896  dscmet 7901  bcthlem33 8014  bcth 8015  isgrp 8024  isgrpi 8025  grpidinvlem3 8033  grpideu 8036  grpidval 8041  grpidinv2 8043  grpinveu 8047  grpinvval 8050  grpinv 8052  isgrp2i 8059  cnid 8112  addinv 8113  mulid 8117  ghgrpilem3 8120  isring 8126  ringi 8127  cnring 8147  ringsn 8148  vci 8152  isvclem 8181  isnvlem 8214  nvi 8218  nvmul0or 8257  nvsubadd 8260  nvsubsub23 8267  nvz 8282  imsmetlem 8309  iporthcom 8355  ipz 8358  lnoval 8399  nmorepnf 8416  nmlno0i 8439  nmlno0 8440  ajfval 8453  hmoval 8454  isphg 8460  isph 8465  ip2eqi 8501  minveceu 8567  minvecdist 8569  pilem1 8654  pilem2 8655  pilem3 8656  pilem4 8657  sinperlem2 8670  cosh111t 8696  efif 8700  efifolem3 8703  efifolem6 8706  efifolem7 8707  efifo 8708  efif1lem6 8714  elcircOLD 8718  efielcirc 8723  circgrp 8724  effoi 8729  logeftb 8748  hvmul0ort 8878  hvsubeq0t 8919  hvaddeq0t 8920  hvaddcant 8921  hvmulcant 8923  hvmulcan2t 8924  hvsubaddt 8928  his6t 8949  hial0 8952  hial02 8953  hi2eqt 8955  orthcom 8958  normlem7tALT 8969  normsub0t 8987  normpytht 8996  hilid 9012  hilidOLD 9013  norm1ex 9110  hhssnv 9122  ocelt 9142  ocsh 9144  ocorth 9152  ocin 9157  occllem5 9165  occllem8 9168  pjthlem13 9219  pjthlem14 9220  pjeq2t 9229  omls 9234  pjoc1t 9255  pjomlt 9257  pjoc2t 9260  choc0 9278  chm0t 9402  chocint 9406  chlejb1t 9423  chlejb2t 9424  chjot 9426  h1deot 9460  h1de2 9464  pjoml6 9522  pjoml2t 9544  pjoml3t 9545  pjcht 9630  pj11t 9650  hods 9692  hodidt 9709  eigortht 9755  nmoprepnf 9785  elunopt 9790  nmfnrepnf 9798  nlfnvalt 9799  adjvalt 9805  eigvecvalt 9813  unopf1ot 9831  elnlfnt 9843  adjt 9848  adjeqt 9850  hmdmadjt 9855  nmlnop0t 9914  lnopeq0 9923  lnopeq 9924  lnopeqt 9925  elunop2t 9929  lnfn0t 9967  riesz4 9987  riesz4t 9988  riesz1t 9989  cnlnadjlem3 9993  cnlnadjlem4 9994  cnlnadjlem5 9995  cnlnadjeut 10002  cnlnssadj 10004  adjbd1o 10009  nmopadjle 10012  hmopidmcht 10072  hmopidmpjt 10073  pjima 10095  pjhmopidm 10101  stelt 10132  hstelt 10133  hstel2t 10137  stadd3 10166  strlem1 10168  str 10175  hstr 10183  large 10185  golem2 10190  stcltr1 10192  superpos 10272  sumdmdi 10333  mddmdin0 10349  elghomlem1 10373  ghomgsg 10386  ghomf1olem 10387  cayleylem3 10402  erdisj2 10436  hmeogrp 10519  rcfpfillem6 10551  dtt2 10569  isded 10620  dedi 10621  cmppfd 10629  domcmpd 10630  codcmpd 10631  iscat 10638  cati 10639  cmpasso 10657  cmpida 10658  cmpidb 10659  ishoma 10666  ishomc 10668  ishomd 10669  ismonb2 10689  cmpmon 10692  isfuna 10699  isfunb 10700  ishgrag 10713  hgralem 10714  ispgrag 10723

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 1459

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

Copyright terms: Public domain