Theorem eqeq1d 1526

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 1524	. 2 |- (A = B -> (A = C <-> B = C))
3	1, 2	syl 10	1 |- (ph -> (A = C <-> B = C))

Syntax hints:   -> wi 3   <-> wb 144   = wceq 992

This theorem is referenced by:  eqeq12d 1532  sbceq2dig 2067  csbieb 2082  uniiunlem 2184  preq12b 2548  iin0 2814  opthgg 2865  opprc3 2873  opth2 2876  opeqsn 2879  frc 2950  frirr 2954  wefrc 2970  onfr 3014  nsuceq0 3053  fneq1 3688  fnun 3700  fnresdisj 3703  funimadisj 3712  foeq1 3775  foco 3790  fvprc 3832  fveq1 3834  fveq2 3835  fvres 3845  funbrfv 3861  fnbrfvb 3864  fvopabn 3897  elrnopabg 3914  dffo3 3933  fconstfv 3963  dff13f 3989  f1fveq 3990  f1ocnvfv3 3997  isofrlem 4015  caoprcan 4116  caoprmo 4131  op2ndg 4149  elrnoprabg 4186  fsplit 4204  tz7.48lem 4256  tz7.49 4260  abianfplem 4262  oe0m1 4296  om0r 4310  oe1m 4315  oawordeulem 4324  oawordeu 4325  omord 4335  oneo 4348  nneob 4395  erth 4422  mapsn 4486  endisj 4578  pw2en 4587  ac6sfilem2 4589  ac6sfilem3 4590  mapenlem2 4637  fodomfib 4710  pm54.43 4715  opthreg 4749  aceq5 4886  kmlem9 4919  zorn2lem7 4940  fodomb 4946  unxpdomlem 4993  cfeq0 5064  cdaung 5073  addnidpi 5182  ltexpi 5183  recmulpq 5224  dmrecpq 5228  ltexpq 5234  halfpq 5236  ltbtwnpq 5238  ltexpri 5303  recexpr 5314  00sr 5362  negexsr 5365  recexsrlem 5366  recexsr 5370  elreal 5404  axrnegex 5437  axrrecex 5438  cnegexlem1 5499  cnegex 5502  addcani 5505  addcan 5506  negeui 5509  subval 5511  subaddi 5525  subadd 5529  subsub23 5530  subid 5549  neg11 5563  negcon1 5564  mul01 5597  add20i 5756  recex 5840  mulcani 5842  mulcant2i 5843  mul0or 5848  muleqadd 5852  receui 5853  divvali 5856  divmuli 5857  divmulzi 5858  divmul 5859  divcan1zi 5870  divcan2zi 5871  divcan1 5872  divne0b 5874  recid 5881  divcan3zi 5899  divcan3 5901  div11 5904  rec11i 5917  rec11r 5918  redivcli 5938  nndiv 6105  zdiv 6356  flbi 6439  modirr 6481  ioo0 6494  icoun 6540  1exp 6779  expeq0 6780  sq11 6826  sqeqor 6846  nn0opth2 6869  sqr00 6915  sqr2irrlem2 6926  sqr2irrlem3 6927  sqr2irrlem5 6929  cru 6939  replim 6962  mulre 6978  abs00 7055  abs1mi 7107  climconst3 7299  ivthlem9 7494  isupivthi 7495  dsupivthlem 7496  efcltlem2 7510  ef0lem 7515  reef11 7617  reeff1olem1 7632  reeff1o 7634  absefib 7693  efieq1re 7694  acdc3 7698  acdc5 7705  unbenlem 7716  ruclem37 7758  infxpidmlem11 7774  retopbas 7865  0ntr 7912  ntreq0 7918  cldlp 7960  ismet 8008  ismsg 8010  msflem 8013  meteq0 8022  metreslem 8032  metxp 8044  methausi 8092  cnmet 8115  blssioo 8124  dscmet 8129  bcthlem33 8242  bcth 8243  isgrp 8254  isgrpi 8255  grpidinvlem3 8263  grpideu 8266  grpidvallem 8274  grpidval 8275  grpidinv2 8277  grpinveu 8281  grpinvval 8284  grpinv 8286  isgrp2i 8293  gx1 8318  gxcom 8325  gxid 8329  cnid 8368  addinv 8369  mulid 8373  ghgrpilem3 8376  isring 8382  ringi 8383  ringideu 8387  cnring 8404  ringsn 8405  vci 8414  isvclem 8443  isnvlem 8476  nvi 8480  nvmul0or 8519  nvsubadd 8522  nvsubsub23 8529  nvz 8544  imsmetlem 8570  vacnlem4 8585  iporthcom 8623  ipz 8626  lnoval 8667  nmorepnf 8685  nmlno0i 8709  nmlno0 8710  ajfval 8724  hmoval 8725  isphg 8732  isph 8737  ip2eqi 8773  ajval 8778  minveceu 8843  minvecdist 8845  pilem1 8938  pilem2 8939  pilem3 8940  pilem4 8941  sinperlem2 8954  sineq0re 8985  cosh111 8989  efif 8993  efifolem3 8996  efifolem6 8999  efifolem7 9000  efifo 9001  efif1lem6 9007  efielcirc 9011  circgrp 9012  effoi 9017  logeftb 9036  hvmul0or 9169  hvsubeq0 9210  hvaddeq0 9211  hvaddcan 9212  hvmulcan 9214  hvmulcanOLD 9215  hvmulcan2 9216  hvsubadd 9220  his6 9241  hial0 9244  hial02 9245  hi2eq 9247  orthcom 9250  normlem7tALT 9261  normsub0 9279  normpyth 9288  hilid 9304  norm1exi 9398  hhssnv 9410  ocel 9430  ocsh 9432  ocorth 9440  ocin 9445  occllem5 9453  occllem8 9456  pjthlem13 9507  pjthlem14 9508  pjeq2 9517  omlsi 9522  pjoc1 9543  pjoml 9545  pjoc2 9548  choc0 9566  chm0 9690  chocin 9694  chlejb1 9711  chlejb2 9712  chjo 9714  h1deoi 9748  h1de2i 9752  pjoml6i 9808  pjoml2 9830  pjoml3 9831  pjch 9917  pj11 9937  hodsi 9981  hodid 9998  eigorth 10044  nmoprepnf 10074  elunop 10079  nmfnrepnf 10087  nlfnval 10088  adjval 10094  eigvecval 10102  unopf1o 10120  elnlfn 10132  adj1 10137  adjeq 10139  hmdmadj 10144  nmlnop0 10202  lnopeq0i 10211  lnopeqi 10212  lnopeq 10213  elunop2 10217  lnfn0 10255  riesz4i 10275  riesz4 10276  riesz1 10277  cnlnadjlem3 10281  cnlnadjlem4 10282  cnlnadjlem5 10283  cnlnadjeu 10290  cnlnssadj 10292  adjbd1o 10297  nmopadjlei 10300  hmopidmch 10361  hmopidmpj 10362  pjimai 10384  pjhmopidm 10390  stel 10422  hstel 10423  hstel2 10427  stadd3i 10456  strlem1 10458  stri 10465  hstri 10473  largei 10475  golem2 10480  stcltr1i 10482  superpos 10562  sumdmdii 10624  mddmdin0i 10640  elghomlem1 10667  ghomgsg 10680  ghomf1olem 10681  cayleylem3 10696  erdisj2 10731  islatalg 10831  labss1 10837  labss2 10839  dupos1 10876  isexid 10893  ismgm 10897  opidon 10898  exidu1 10902  idrval 10904  cmpidelt 10906  rngmgmbs4 10945  ununr 10955  zrdivrng 10969  vri 10981  hmeogrp 11044  eqindhome 11047  subspemp2 11061  rcfpfillem6 11094  limfillem1 11101  dtt2 11110  iscomp 11114  bwt2 11123  isded 11190  dedi 11191  cmppfd 11199  domcmpd 11200  codcmpd 11201  iscat 11208  cati 11209  cmpasso 11227  cmpida 11228  cmpidb 11229  ishoma 11242  ishomc 11244  ishomd 11245  ismonb2 11267  cmpmon 11270  isepib2 11277  cinvlem3 11284  isfuna 11288  isfunb 11289  subtr 11395  elfiun 11421  fictb 11423  inficlALT 11424  ordtypelem4 11430  ordtypelem5 11431  ordtypelem6 11432  omsubinit 11451  opnbnd 11461  cldbnd 11462  hausnei2 11471  compsublem 11487  compsub 11488  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  dfcon2 11501  connsub 11502  2ndcsb 11537  isfne 11541  isref 11549  topfneec2 11563  islocfin 11567  isnrm2 11613  nrmsep 11615  nrmsep2 11616  filrn 11643  filssufil 11656  ufinffr 11663  limfil 11675  sfcls 11716  filclus 11717  fcluscf 11724  flimfnfcls 11727  filnetlem5 11767  isgalem 11771  ssga 11777  gapmlem 11783  f1elima 11818  findcard 11836  add20 11858  divexp 11859  mod0 11871  absmod0 11873  sdclem1 11875  sdc 11877  fsum00 11883  iserzshft2 11892  fsumlt1 11894  metf1o 11907  sstotbnd 11992  ismtyval 12003  ismtyhmeolem 12006  heiborlem10 12020  heiborlem11 12021  heiborlem13 12023  heiborlem42 12052  bfplem11 12064  rrnmet 12072  rrntotbnd 12078  phtpyval 12089  isphtpy 12090  phtpycom 12092  phtpyco 12098  isphtpc 12101  ishgrag 12195  hgralem 12196  ispgrag 12205

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1511

Copyright terms: Public domain