Theorem opreq2d 3974

Description: Equality deduction for operation value.

Hypothesis

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

Assertion

Ref	Expression
opreq2d	|- (ph -> (CFA) = (CFB))

Proof of Theorem opreq2d

Step	Hyp	Ref	Expression
1		opreq1d.1	. 2 |- (ph -> A = B)
2		opreq2 3967	. 2 |- (A = B -> (CFA) = (CFB))
3	1, 2	syl 10	1 |- (ph -> (CFA) = (CFB))

Syntax hints:   -> wi 3   = wceq 956  (class class class)co 3961

This theorem is referenced by:  opreq12d 3976  csbopr1g 3986  caoprass 4052  caoprdistr 4057  oaass 4193  odi 4208  omass 4209  nnmsucr 4238  ecoprass 4318  ecoprdi 4319  addasspi 5011  mulasspi 5013  distrpi 5014  addclprlem2 5107  mulclprlem 5109  distrlem4pr 5118  1idpr 5121  prlem934a 5125  prlem936a 5141  prlem936 5143  mulcmpblnrlem 5170  ssgt0sr 5205  supsrlem4 5216  supsr 5219  mulcnsr 5242  ax1id 5270  axcnre 5274  add23t 5325  add42t 5327  cnegext 5336  negsubt 5370  addsubasst 5371  subnegt 5382  pncant 5385  mul23t 5407  muladdt 5409  subdit 5415  mul2negt 5442  negdit 5443  negsubdit 5445  submul2t 5448  subsub2t 5449  subsub4t 5452  sub23t 5453  nnncant 5454  nppcan2t 5458  addsub4t 5461  sub4t 5464  mulsubt 5465  pnncant 5468  divcan2t 5704  divrecz 5715  divrect 5716  divasst 5718  divdirt 5727  divdirtOLD 5728  divsubdirt 5746  recrect 5747  divmul24t 5754  divadddivt 5755  divdivdivt 5756  divcan6t 5762  divdivmult 5766  conjmult 5768  nnmulclt 5909  flhalft 6213  quorem 6218  seq1val 6276  seq1suclem 6280  seq1m1 6283  ser1p1 6300  shftcan1t 6318  seq1shftid 6320  icoshftf1olem 6370  seq0fval 6495  seqzfval 6497  seqzp1 6508  seqzm1 6509  seq0p1 6511  seqzval2t 6513  ser0p1 6527  expvalt 6530  expp1t 6534  expm1t 6543  recexpt 6555  expaddt 6556  expmult 6557  expsubt 6558  divexpt 6559  expordit 6560  subsq2t 6603  binom2t 6610  bernneq 6612  discrlem2 6617  discrlem3 6618  discrlem 6619  nn0opth 6626  sqrmul 6665  sqr2irrlem2 6685  sqr2irrlem3 6686  sqr2irrlem5 6688  cru 6697  crut 6698  crrecz 6701  creur 6702  creui 6703  replimt 6721  cjvalt 6723  imret 6733  reim0bt 6735  rereb 6738  readdt 6763  resubt 6764  imaddt 6766  imsubt 6767  cjaddt 6770  cjmult 6771  addcjt 6773  cjsubt 6774  recjt 6776  cj11t 6788  absnegt 6790  abscjt 6792  abs00 6800  sqabsaddt 6806  sqabssubt 6807  absmult 6816  absdivt 6818  absret 6824  absresqt 6825  recvalz 6845  cjdiv 6846  cjdivt 6847  absmaxt 6855  abstrit 6856  recant 6863  abslem2 6867  cau2 6871  ser1absdiflem 6887  facp1t 6894  facnn2t 6897  faclbnd 6903  faclbnd4lem1 6906  faclbnd4lem2 6907  faclbnd4lem3 6908  faclbnd4lem4 6909  faclbnd6 6912  bcvalt 6916  bccmplt 6920  bcn0t 6921  bcnnt 6922  bcnp11t 6923  bcnp1nt 6924  bcpasc2t 6926  bcpasc 6927  bcpasct 6928  sumeq2 6943  fsump1slem 6970  fsum1ps 6976  fsum3 6982  fsum4 6983  fsumrev 6987  fsummulc1 6991  fsumconst 6996  fsumabs 7001  ser1ser0 7006  serz1p 7010  serzmulc1 7015  serzmulc 7016  serzrelem 7019  binomlem1 7024  binomlem2 7025  binomlem3 7026  binomlem4 7027  binomlem5 7028  binomlem6 7029  binom 7030  binom1p 7031  bcxmas 7034  climaddc1 7076  climsub 7088  caucvg 7121  caucvg3a 7122  caucvg3lem 7124  caucvg3 7125  caucvg3t 7126  serzf0 7127  ser1f0 7128  ser1const 7129  ser1cmp2 7135  cvgcmp2lem 7138  cvgcmp2 7139  cvgcmp2c 7141  cvgcmp3ce 7145  cvgcmp3cetlem1 7146  cvgcmp3cetlem2 7147  isummulc1 7170  isummulc1ALT 7171  isummulc1a 7172  infcvglem2 7180  infcvg 7182  fnsmnt 7184  geoser 7192  geolimilem 7193  geolimi 7194  geolim 7195  geolim1 7197  georeclim 7198  geoisumr 7201  geoisum1c 7203  0.999... 7204  cvgratlem1ALT 7205  cvgratlem3ALT 7207  cvgratlem1 7208  cvgratlem3 7210  cvgratlem4 7211  cvgratlem5 7212  fsum0diaglem2 7215  fsum0diag 7216  fsum0diag2 7217  fsum0diag4 7219  efcltlem1 7262  efcltlem2 7263  efseq1ex 7264  ef0lem 7268  erelem2 7278  erelem3 7279  ege2lem2 7286  ege2le3lem2 7287  efaddlem6 7301  efaddlem17 7312  efaddt 7325  efsubt 7329  efexpt 7330  eftlext 7336  ef1tllem 7339  ef01tllem1 7341  ef01tllem2 7342  ef01tllem2OLD 7343  eirrlem2 7348  eirrlem5 7351  eflegeot 7373  efcnlem4 7379  resinvalt 7390  recosvalt 7391  efi4pt 7392  efivalt 7404  efmivalt 7405  efeult 7406  sinaddt 7410  cosaddt 7411  sinsubt 7412  cossubt 7413  sincossqt 7418  sin2tt 7419  cos2tt 7420  sin01bndlem3 7426  cos01bndlem3 7428  demoivre 7441  acdc3lem 7443  acdc2lem2 7446  acdc2 7447  acdc5lem2 7449  acdc5 7450  acdclem 7451  ruclem4 7470  ruclem32 7498  cnfval 7713  cnpfval 7714  mettri2 7770  mettri4 7771  metsym 7773  mettri3 7775  metxpdval 7786  metxplem4 7790  metxp 7791  tgioolem 7871  iscau3 7895  iscau4 7897  opr1cn 7935  bcthlem1 7956  bcthlem17 7972  bcthlem20 7975  isgrp 7998  grpass 8004  grpidinvlem2 8006  grpinvid2 8030  isgrp2i 8033  grpinvop 8037  grpdivfval 8038  grpdivval 8039  grpdivinv 8040  grpdivdiv 8044  grpmuldivass 8045  grppncan 8047  grpnpcan 8048  grppnpcan2 8049  abl23 8061  abldivdiv4 8066  abldiv23 8067  ablnnncan 8068  issubgi 8079  grpsn 8081  ablmul 8088  ghgrpilem1 8090  ghgrpilem4 8093  isring 8098  ringi 8099  ringdi 8103  ringdir 8104  ringass 8105  ringsn 8120  vci 8124  vcdi 8128  vcdir 8129  vcass 8130  vcsubdir 8132  vcz 8146  vcm 8147  vcrinv 8148  vcnegsubdi2 8151  vcsub4 8152  isvclem 8153  vcoprne 8155  isnvlem 8186  nvi 8190  nvmval 8220  nvmfval 8221  nvmdi 8227  nvrinv 8230  nvsubadd 8232  nvaddsub4 8238  nvnncan 8240  nvs 8247  nvdif 8250  nvpi 8251  nvtri 8255  nvmtri 8256  nvabs 8258  nvge0 8259  cnnvm 8270  nvnd 8276  imsmetlem 8280  ipfval 8309  ipval 8310  ipval2lem3 8312  ipval2 8314  4ipval2 8315  ipval3 8316  ipval2lem6 8318  4ipval3 8319  ipid 8320  ipcj 8324  ipipcj 8325  ip0r 8327  ip1cnilem4 8333  ip1cnilem6 8335  sspmval 8349  sspival 8354  lnoval 8370  islno 8371  lnolin 8372  lno0 8374  lnocoi 8375  lnoadd 8376  0lno 8407  nmlnoubi 8413  nmblolbii 8416  blometi 8420  blocnilem 8421  isphg 8433  cnph 8435  isph 8438  phpar2 8439  phpar 8440  ipdiri 8446  ipasslem1 8447  ipasslem2 8448  ipasslem5 8451  ipasslem11 8457  ipassi 8458  ipass 8462  ipassr 8463  ipsubdir 8465  pythi 8467  siilem1 8468  siilem2 8469  siii 8470  sii 8471  sspph 8472  ipblnfi 8473  ajmoi 8476  ubthlem8 8493  ubthlem10 8495  minveclem6 8507  minveclem8 8509  minveclem19 8520  minveclem21 8522  minveclem23 8524  minveclem30 8531  minveclem36 8537  minveceu 8540  htthlem2 8578  htthlem3 8579  sinper 8647  cosper 8648  efimpi 8655  efifolem2 8678  efifolem3 8679  efifolem6 8682  shftefif1olem 8696  effoi 8700  efper 8702  hvsubvalt 8841  hvaddsubvalt 8857  hvadd23t 8858  hvsub4t 8861  hvaddsub12t 8862  hvpncant 8863  hvaddsubasst 8865  hvsubdistr1t 8871  hvsubdistr2t 8872  hvsubsub4t 8882  hvnegdit 8889  hvaddsub4t 8900  his5t 8908  his2subt 8913  normlem6 8936  normlem9at 8942  norm-iit 8960  norm-iiit 8962  normpyth 8964  normpytht 8967  norm3dift 8972  norm3adift 8975  normpart 8977  polidt 8981  hhph 9000  bcsALT 9001  bcst 9003  hcau2 9010  hhssnv 9089  chocuni 9127  occllem2 9129  projlem7 9147  projlem17 9157  projlem20 9160  projlem22 9162  projlem26 9166  pjthlem8 9181  pjthlem9 9182  omlsilem 9199  pjch 9220  chdmm1t 9403  chdmm3t 9405  chdmm4t 9406  chjasst 9411  chj4t 9413  ledit 9418  spanunt 9423  h1de2b 9432  pjspansnt 9455  spanunsn 9457  hosmvalt 9466  hommvalt 9467  hodmvalt 9468  hfsmvalt 9469  hfmmvalt 9470  homvalt 9473  hfmvalt 9477  cmcmlem 9489  pjoml2t 9509  spansnjt 9547  spansncvt 9553  5oalem1 9554  5oalem2 9555  5oalem3 9556  5oalem5 9558  3oalem2 9563  pjcj 9584  pjadjt 9585  pjaddt 9586  pjsubt 9588  pjmult 9589  pjcjt2 9592  pjopytht 9620  hoaddass 9657  hoaddasst 9663  hoadd23t 9664  hocsubdirt 9666  hoaddid1 9667  honegsub 9677  ho0subt 9678  honegsubt 9680  homco1t 9682  homulasst 9683  hoadddit 9684  hosubnegt 9688  hosubdit 9689  honegsubdit 9691  hosubsub2t 9693  hosub4t 9694  hoaddsubasst 9696  hosubsub4t 9699  adjsymt 9714  eigortht 9719  ellnopt 9739  elhmopt 9755  ellnfnt 9765  adjvalt 9769  cnopct 9792  lnoplt 9793  unopt 9794  unopadjt 9798  unoplint 9799  hmopt 9801  cnfnct 9809  lnfnlt 9810  adjt 9812  adjeqt 9814  hmoplint 9821  bramult 9825  brafnmult 9830  kbpjt 9835  lnopmult 9846  lnopaddmul 9852  lnopsubmul 9854  homco2t 9856  0hmop 9862  0lnfn 9864  hoddit 9870  adj0 9874  lnopm 9880  lnophs 9881  lnopco 9883  lnopeq0lem2 9886  lnopeq0 9887  lnopuni 9892  lnophm 9898  lnophmt 9899  hmopst 9900  hmopmt 9901  hmopcot 9903  nmbdoplb 9904  nmcoplb 9913  lnopcon 9918  lnfnaddmul 9929  lnfnsub 9930  lnfnmult 9932  nmbdfnlb 9933  nmcfnlb 9942  lnfncon 9945  nlelsh 9948  cnlnadjlem2 9956  cnlnadjlem5 9959  cnlnadjlem6 9960  cnlnadjlem9 9963  cnlnssadj 9968  adjlnopt 9974  adjmult 9980  adjaddt 9981  nmopco 9983  adjco 9988  unierr 9992  branmfnt 9993  cnvbravalt 9998  cnvbramult 10003  kbass6t 10009  leopnmidt 10026  hmopidmch 10034  hmopidmpj 10035  pjadjco 10044  pjss2co 10047  pjclem4 10082  pjadj2co 10087  pj3s 10090  pj3cor1 10092  hstel2t 10101  hst1ht 10109  hstlet 10112  hstoht 10114  stjt 10117  st0 10131  stcltrlem1 10158  mdbrt 10176  dmdmdt 10182  ssmd1 10193  ssmd2 10194  mdslmd1lem2 10208  mdslmd3 10214  cvexchlem 10250  atoml2 10265  irredlem3 10274  atcvat3 10278  atabs 10283  sumdmdlem2 10301  cdj1 10315  cdj3lem1 10316  cdj3lem2b 10319  cdj3lem3b 10322  cdj3 10323  ghomgrpilem1 10340  ghomlin 10348  symggrpi 10361  cayleylem2 10365  hmeogrp 10480  mslb1 10541  iscat 10599  cati 10600  1cat 10604  cmpasso 10618  cmpidb 10620

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2701  ax-pow 2740  ax-pr 2777

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-v 1810  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-nul 2279  df-pw 2400  df-sn 2410  df-pr 2411  df-op 2414  df-uni 2502  df-br 2618  df-opab 2665  df-xp 3182  df-cnv 3184  df-dm 3186  df-rn 3187  df-res 3188  df-ima 3189  df-fv 3196  df-opr 3963

Copyright terms: Public domain