Theorem opreq2d 3961

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

Syntax hints:   -> wi 3   = wceq 953  (class class class)co 3948

This theorem is referenced by:  opreq12d 3963  csbopr1g 3973  caoprass 4040  caoprdistr 4045  oaass 4179  odi 4194  omass 4195  nnmsucr 4224  ecoprass 4304  ecoprdi 4305  addasspi 4995  mulasspi 4997  distrpi 4998  addclprlem2 5091  mulclprlem 5093  distrlem4pr 5102  1idpr 5105  prlem934a 5109  prlem936a 5125  prlem936 5127  mulcmpblnrlem 5154  ssgt0sr 5189  supsrlem4 5200  supsr 5203  mulcnsr 5226  ax1id 5254  axcnre 5258  add23t 5309  add42t 5311  cnegext 5320  negsubt 5354  addsubasst 5355  subnegt 5366  pncant 5369  mul23t 5391  muladdt 5393  subdit 5399  mul2negt 5426  negdit 5427  negsubdit 5429  submul2t 5432  subsub2t 5433  subsub4t 5436  sub23t 5437  nnncant 5438  nppcan2t 5442  addsub4t 5445  sub4t 5448  mulsubt 5449  pnncant 5452  divcan2t 5690  divrecz 5701  divrect 5702  divasst 5704  divdirt 5713  divsubdirt 5731  recrect 5732  divmul24t 5739  divadddivt 5740  divdivdivt 5741  divcan6t 5747  divdivmult 5751  conjmult 5753  nnmulclt 5889  flhalft 6189  seq1val 6249  seq1suclem 6253  seq1m1 6256  ser1p1 6273  shftcan1t 6291  seq1shftid 6293  icoshftf1olem 6343  seq0fval 6467  seqzfval 6469  seqzp1 6480  seqzm1 6481  seq0p1 6483  seqzval2t 6485  ser0p1 6499  expvalt 6502  expp1t 6506  expm1t 6515  recexpt 6526  expaddt 6527  expmult 6528  expsubt 6529  divexpt 6530  expordit 6531  subsq2t 6574  binom2t 6581  bernneq 6583  discrlem2 6587  discrlem3 6588  discrlem 6589  nn0opth 6596  sqrmul 6635  sqr2irrlem2 6655  sqr2irrlem3 6656  sqr2irrlem5 6658  cru 6667  crut 6668  crutOLD 6669  crrecz 6672  creur 6673  creui 6674  replimt 6692  replimtOLD 6693  cjvalt 6695  imret 6710  reim0bt 6712  rereb 6715  readdt 6740  resubt 6741  imaddt 6743  imsubt 6744  cjaddt 6747  cjmult 6748  addcjt 6750  cjsubt 6751  recjt 6753  cj11t 6765  absnegt 6767  abscjt 6769  abs00 6777  sqabsaddt 6783  sqabssubt 6784  absmult 6793  absdivt 6795  absret 6801  absresqt 6802  recvalz 6825  cjdiv 6826  cjdivt 6827  abstrit 6835  abslem2 6846  cau2 6850  ser1absdiflem 6866  facp1t 6873  facnn2t 6876  faclbnd 6882  faclbnd4lem1 6885  faclbnd4lem2 6886  faclbnd4lem3 6887  faclbnd4lem4 6888  faclbnd6 6891  bcvalt 6895  bccmplt 6900  bcn0t 6901  bcnnt 6902  bcnp11t 6903  bcnp1nt 6904  bcpasc2t 6906  bcpasc 6907  bcpasct 6908  sumeq2 6923  fsump1slem 6950  fsum1ps 6956  fsum3 6962  fsum4 6963  fsumrev 6967  fsummulc1 6971  fsumconst 6976  fsumabs 6981  ser1ser0 6986  serz1p 6990  serzmulc1 6995  serzmulc 6996  serzrelem 6999  binomlem1 7004  binomlem2 7005  binomlem3 7006  binomlem4 7007  binomlem5 7008  binomlem6 7009  binom 7010  binom1p 7011  bcxmas 7014  climaddc1 7054  climsub 7066  caucvg 7099  caucvg3 7103  caucvg3t 7104  serzf0 7105  ser1f0 7106  ser1const 7107  ser1cmp2 7113  cvgcmp2lem 7116  cvgcmp2 7117  cvgcmp2c 7119  cvgcmp3ce 7123  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  isummulc1 7147  isummulc1ALT 7148  isummulc1a 7149  infcvglem2 7157  infcvg 7159  fnsmnt 7161  geoser 7169  geolimilem 7170  geolimi 7171  geolim 7172  geolim1 7174  georeclim 7175  geoisumr 7178  geoisum1c 7180  0.999... 7181  cvgratlem1ALT 7182  cvgratlem3ALT 7184  cvgratlem1 7185  cvgratlem3 7187  cvgratlem4 7188  cvgratlem5 7189  fsum0diaglem2 7192  fsum0diag 7193  fsum0diag2 7194  fsum0diag4 7196  efcltlem1 7246  efcltlem2 7247  efseq1ex 7248  ef0lem 7252  erelem2 7262  erelem3 7263  ege2lem2 7270  ege2le3lem2 7271  efaddlem6 7285  efaddlem17 7296  efaddt 7309  efsubt 7313  efexpt 7314  eftlext 7320  ef1tllem 7323  ef01tllem1 7325  ef01tllem2 7326  eirrlem2 7331  eirrlem5 7334  eflegeot 7356  efcnlem4 7362  resinvalt 7375  recosvalt 7376  efi4pt 7377  efivalt 7389  efmivalt 7390  efeult 7391  sinaddt 7395  cosaddt 7396  sinsubt 7397  cossubt 7398  sincossqt 7403  sin2tt 7404  cos2tt 7405  sin01bndlem3 7411  cos01bndlem3 7413  demoivre 7426  acdc3lem 7428  acdc2lem2 7431  acdc2 7432  acdc5lem2 7434  acdc5 7435  acdclem 7436  ruclem4 7456  ruclem32 7484  cnfval 7696  cnpfval 7697  mettri2 7752  mettri4 7753  metsym 7755  mettri3 7758  mettri3OLD 7759  metxpdval 7769  metxplem4 7773  metxp 7774  tgioolem 7853  iscau3 7876  opr1cn 7912  bcthlem1 7933  bcthlem17 7949  bcthlem20 7952  isgrp 7975  grpass 7981  grpidinvlem2 7983  grpinvid2 8007  isgrp2i 8011  grpinvop 8015  grpdivfval 8016  grpdivval 8017  grpdivinv 8018  grpdivdiv 8022  grpmuldivass 8023  grppncan 8025  grpnpcan 8026  grppnpcan2 8027  abl23 8040  abldivdiv4 8046  abldiv23 8047  ablnnncan 8048  issubgi 8059  grpsn 8061  ablmul 8068  ghgrpilem1 8070  ghgrpilem4 8073  isring 8078  ringi 8079  ringdi 8083  ringdir 8084  ringass 8085  ringsn 8100  vci 8104  vcdi 8108  vcdir 8109  vcass 8110  vcsubdir 8112  vcz 8126  vcm 8127  vcrinv 8128  vcnegsubdi2 8131  vcsub4 8132  isvcgOLD 8133  isvclem 8134  vcoprne 8136  isnvlem 8167  isnvgOLD 8168  nvi 8173  nvmval 8203  nvmfval 8204  nvmdi 8210  nvrinv 8213  nvsubadd 8215  nvaddsub4 8221  nvnncan 8223  nvs 8229  nvdif 8232  nvpi 8233  nvtri 8237  nvmtri 8238  nvabs 8240  nvge0 8241  cnnvm 8251  nvnd 8257  imsmetlem 8261  ipfval 8286  ipval 8287  ipval2lem3 8289  ipval2 8291  4ipval2 8292  ipval3 8293  ipval2lem6 8295  4ipval3 8296  ipid 8297  ipcj 8301  ipipcj 8302  ip0r 8304  ip1cnilem4 8310  ip1cnilem6 8312  sspmval 8326  sspival 8331  lnoval 8347  islno 8348  lnolin 8349  lno0 8351  lnocoi 8352  0lno 8382  nmlnoubi 8388  nmblolbii 8390  blometi 8394  blocnilem 8395  isphg 8407  cnph 8409  isph 8412  phpar2 8413  phpar 8414  ipdiri 8420  ipasslem1 8421  ipasslem2 8422  ipasslem5 8425  ipasslem11 8431  ipassi 8432  ipass 8436  ipassr 8437  ipsubdir 8439  pythi 8441  siilem1 8442  siilem2 8443  siii 8444  sii 8445  sspph 8446  ipblnfi 8447  ajmoi 8450  ubthlem8 8467  ubthlem10 8469  minveclem6 8481  minveclem8 8483  minveclem19 8494  minveclem21 8496  minveclem23 8498  minveclem30 8505  minveclem36 8511  minveceu 8514  htthlem2 8551  htthlem3 8552  sinper 8609  cosper 8610  efimpi 8615  efifolem2 8638  efifolem3 8639  efifolem6 8642  circgrpOLD 8658  shftefif1olem 8661  shftefif1olemOLD 8662  effoi 8666  effoiOLD 8667  efper 8669  hvsubvalt 8807  hvaddsubvalt 8823  hvadd23t 8824  hvsub4t 8827  hvaddsub12t 8828  hvpncant 8829  hvaddsubasst 8831  hvsubdistr1t 8837  hvsubdistr2t 8838  hvsubsub4t 8848  hvnegdit 8855  hvaddsub4t 8866  his5t 8874  his2subt 8879  normlem6 8902  normlem9at 8908  norm-iit 8926  norm-iiit 8928  normpyth 8930  normpytht 8933  norm3dift 8938  norm3adift 8941  normpart 8943  polidt 8947  hhph 8966  bcsALT 8967  bcst 8969  hcau2 8976  hhssnv 9054  chocuni 9088  occllem2 9090  projlem7 9108  projlem17 9118  projlem20 9121  projlem22 9123  projlem26 9127  pjthlem8 9141  pjthlem9 9142  omlsilem 9159  pjch 9180  chdmm1t 9363  chdmm3t 9365  chdmm4t 9366  chjasst 9371  chj4t 9373  ledit 9378  spanunt 9383  h1de2b 9392  h1de2bOLD 9393  pjspansnt 9417  spanunsn 9419  hosmvalt 9428  hommvalt 9429  hodmvalt 9430  hfsmvalt 9431  hfmmvalt 9432  homvalt 9435  hfmvalt 9439  cmcmlem 9451  pjoml2t 9471  spansnjt 9509  spansncvt 9515  5oalem1 9516  5oalem2 9517  5oalem3 9518  5oalem5 9520  3oalem2 9525  pjcj 9546  pjadjt 9547  pjaddt 9548  pjsubt 9550  pjmult 9551  pjcjt2 9554  pjopytht 9582  hoaddass 9619  hoaddasst 9625  hoadd23t 9626  hocsubdirt 9628  hoaddid1 9629  honegsub 9639  ho0subt 9640  honegsubt 9642  homco1t 9644  homulasst 9645  hoadddit 9646  hosubnegt 9650  hosubdit 9651  honegsubdit 9653  hosubsub2t 9655  hosub4t 9656  hoaddsubasst 9658  hosubsub4t 9661  adjsymt 9676  eigortht 9681  ellnopt 9701  elhmopt 9717  ellnfnt 9727  adjvalt 9731  cnopct 9753  lnoplt 9754  unopt 9755  unopadjt 9759  unoplint 9760  hmopt 9762  cnfnct 9770  lnfnlt 9771  adjt 9773  adjeqt 9775  hmoplint 9782  bramult 9786  brafnmult 9791  kbpjt 9796  lnopmult 9807  lnopaddmul 9813  lnopsubmul 9815  homco2t 9817  0hmop 9823  0lnfn 9825  hoddit 9830  adj0 9834  lnopm 9840  lnophs 9841  lnopco 9843  lnopeq0lem2 9846  lnopeq0 9847  lnopuni 9852  lnophm 9858  lnophmt 9859  hmopst 9860  hmopmt 9861  hmopcot 9863  nmbdoplb 9864  nmcoplb 9873  lnopcon 9878  lnfnaddmul 9889  lnfnsub 9890  lnfnmult 9892  nmbdfnlb 9893  nmcfnlb 9902  lnfncon 9905  nlelsh 9908  cnlnadjlem2 9916  cnlnadjlem5 9919  cnlnadjlem6 9920  cnlnadjlem9 9923  cnlnssadj 9928  adjlnopt 9934  adjmult 9939  adjaddt 9940  nmopco 9942  adjco 9947  unierr 9950  branmfnt 9951  cnvbravalt 9956  cnvbramult 9960  kbass6t 9966  leopnmidt 9982  hmopidmch 9990  hmopidmpj 9991  pjadjco 10000  pjss2co 10003  pjclem4 10037  pjadj2co 10042  pj3s 10045  pj3cor1 10047  hstel2t 10056  hst1ht 10064  hstlet 10067  hstoht 10069  stjt 10072  st0 10086  stcltrlem1 10113  mdbrt 10131  dmdmdt 10137  ssmd1 10146  ssmd2 10147  mdslmd1lem2 10161  mdslmd3 10167  cvexchlem 10203  atoml2 10218  irredlem3 10227  atcvat3 10231  atabs 10236  sumdmdlem2 10253  cdj1 10265  cdj3lem1 10266  cdj3lem2b 10269  cdj3lem3b 10272  cdj3 10273  ghomgrpilem1 10290  ghomlin 10298  symggrpiOLD 10311  symggrpi 10313  cayleylem2 10317  hmeogrp 10425  mslb1 10473  iscat 10531  cati 10532  1cat 10536  cmpasso 10550  cmpidb 10552

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-xp 3174  df-cnv 3176  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fv 3188  df-opr 3950

Copyright terms: Public domain