Theorem opreq2d 3982

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

Syntax hints:   -> wi 3   = wceq 958  (class class class)co 3969

This theorem is referenced by:  opreq12d 3984  csbopr1g 3994  caoprass 4060  caoprdistr 4065  oaass 4201  odi 4216  omass 4217  nnmsucr 4246  ecoprass 4326  ecoprdi 4327  addasspi 5035  mulasspi 5037  distrpi 5038  addclprlem2 5131  mulclprlem 5133  distrlem4pr 5142  1idpr 5145  prlem934a 5149  prlem936a 5165  prlem936 5167  mulcmpblnrlem 5194  ssgt0sr 5229  supsrlem4 5240  supsr 5243  mulcnsr 5266  ax1id 5294  axcnre 5298  add23t 5349  add42t 5351  cnegext 5360  negsubt 5394  addsubasst 5395  subnegt 5406  pncant 5409  mul23t 5431  muladdt 5433  subdit 5439  mul2negt 5466  negdit 5467  negsubdit 5469  submul2t 5472  subsub2t 5473  subsub4t 5476  sub23t 5477  nnncant 5478  nppcan2t 5482  addsub4t 5485  sub4t 5488  mulsubt 5489  pnncant 5492  divcan2tOLD 5734  divrecz 5745  divrect 5746  divasst 5748  divdirt 5757  divdirtOLD 5758  divsubdirt 5776  divsubdirtOLD 5777  recrect 5778  divmul24t 5785  divadddivt 5786  divdivdivt 5787  divcan6t 5793  divdivmult 5797  conjmult 5799  nnmulclt 5943  flhalft 6248  quoremz 6253  seq1val 6313  seq1suclem 6317  seq1m1 6320  ser1p1 6337  shftcan1t 6355  seq1shftid 6357  icoshftf1olem 6411  seq0fval 6536  seqzfval 6538  seqzp1 6549  seqzm1 6550  seq0p1 6552  seqzval2t 6554  ser0p1 6568  expvalt 6571  expp1t 6575  expm1t 6584  recexpt 6596  expaddt 6597  expmult 6598  expsubt 6599  divexpt 6600  expordit 6601  subsq2t 6644  binom2t 6651  bernneq 6653  discrlem2 6658  discrlem3 6659  discrlem 6660  nn0opth 6667  sqrmul 6706  sqr2irrlem2 6726  sqr2irrlem3 6727  sqr2irrlem5 6729  cru 6738  crut 6739  crrecz 6742  creur 6743  creui 6744  replimt 6762  cjvalt 6764  imret 6774  reim0bt 6776  rerebt 6777  readdt 6805  resubt 6806  imaddt 6808  imsubt 6809  cjaddt 6812  cjmult 6813  addcjt 6815  cjsubt 6816  recjt 6818  cj11t 6830  absnegt 6832  abscjt 6834  abs00 6842  sqabsaddt 6848  sqabssubt 6849  absmult 6858  absdivt 6860  absret 6866  absresqt 6867  recvalz 6887  cjdiv 6888  cjdivt 6889  absmaxt 6897  abstrit 6898  recant 6905  abslem2 6909  cau2 6913  ser1absdiflem 6929  facp1t 6936  facnn2t 6939  faclbnd 6945  faclbnd4lem1 6948  faclbnd4lem2 6949  faclbnd4lem3 6950  faclbnd4lem4 6951  faclbnd6 6954  bcvalt 6958  bccmplt 6962  bcn0t 6963  bcnnt 6964  bcnp11t 6965  bcnp1nt 6966  bcpasc2t 6968  bcpasc 6969  bcpasct 6970  sumeq2 6985  fsump1slem 7012  fsum1ps 7018  fsum3 7024  fsum4 7025  fsumrev 7029  fsummulc1 7033  fsumconst 7038  fsumabs 7043  ser1ser0 7048  serz1p 7052  serzmulc1 7057  serzmulc 7058  serzrelem 7061  binomlem1 7066  binomlem2 7067  binomlem3 7068  binomlem4 7069  binomlem5 7070  binomlem6 7071  binom 7072  binom1p 7073  bcxmas 7076  climaddc1 7118  climsub 7130  caucvg 7163  caucvg3a 7164  caucvg3lem 7166  caucvg3 7167  caucvg3t 7168  serzf0 7169  ser1f0 7170  ser1const 7171  ser1cmp2 7177  cvgcmp2lem 7180  cvgcmp2 7181  cvgcmp2c 7183  cvgcmp3ce 7187  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  isummulc1 7212  isummulc1ALT 7213  isummulc1a 7214  infcvglem2 7222  infcvg 7224  fnsmnt 7226  geoser 7234  geolimilem 7235  geolimi 7236  geolim 7237  geolim1 7239  georeclim 7240  geoisumr 7243  geoisum1c 7245  0.999... 7246  cvgratlem1ALT 7247  cvgratlem3ALT 7249  cvgratlem1 7250  cvgratlem3 7252  cvgratlem4 7253  cvgratlem5 7254  fsum0diaglem2 7257  fsum0diag 7258  fsum0diag2 7259  fsum0diag4 7261  efcltlem1 7304  efcltlem2 7305  efseq1ex 7306  ef0lem 7310  erelem2 7320  erelem3 7321  ege2lem2 7328  ege2le3lem2 7329  efaddlem6 7343  efaddlem17 7354  efaddt 7367  efsubt 7371  efexpt 7372  eftlext 7378  ef1tllem 7381  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  eirrlem2 7390  eirrlem5 7393  eflegeot 7416  efcnlem4 7422  resinvalt 7433  recosvalt 7434  efi4pt 7435  efivalt 7447  efmivalt 7448  efeult 7449  sinaddt 7453  cosaddt 7454  sinsubt 7455  cossubt 7456  sincossqt 7461  sin2tt 7462  cos2tt 7463  cos2tsint 7464  sin01bndlem3 7470  cos01bndlem3 7472  demoivre 7485  acdc3lem 7487  acdc2lem2 7490  acdc2 7491  acdc5lem2 7493  acdc5 7494  acdclem 7495  ruclem4 7514  ruclem32 7542  cnfval 7753  cnpfval 7754  mettri2 7810  mettri4 7811  metsym 7813  mettri3 7815  metxpdval 7826  metxplem4 7830  metxp 7831  tgioolem 7911  iscau3 7935  iscau4 7937  opr1cn 7975  bcthlem1 7996  bcthlem17 8012  bcthlem20 8015  isgrp 8038  grpass 8044  grpidinvlem2 8046  grpinvid2 8069  isgrp2i 8072  grpinvop 8076  grpdivfval 8077  grpdivval 8078  grpdivinv 8079  grpdivdiv 8083  grpmuldivass 8084  grppncan 8086  grpnpcan 8087  grppnpcan2 8088  abl23 8100  abldivdiv4 8105  abldiv23 8106  ablnnncan 8107  issubgi 8118  grpsn 8120  ablmul 8127  ghgrpilem1 8129  ghgrpilem4 8132  isring 8137  ringi 8138  ringdi 8142  ringdir 8143  ringass 8144  ringsn 8159  vci 8163  vcdi 8167  vcdir 8168  vcass 8169  vcsubdir 8171  vcz 8185  vcm 8186  vcrinv 8187  vcnegsubdi2 8190  vcsub4 8191  isvclem 8192  vcoprne 8194  isnvlem 8225  nvi 8229  nvmval 8259  nvmfval 8260  nvmdi 8266  nvrinv 8269  nvsubadd 8271  nvaddsub4 8277  nvnncan 8279  nvs 8286  nvdif 8289  nvpi 8290  nvtri 8294  nvmtri 8295  nvabs 8297  nvge0 8298  cnnvm 8309  nvnd 8315  imsmetlem 8319  ipfval 8348  ipval 8349  ipval2lem3 8351  ipval2 8353  4ipval2 8354  ipval3 8355  ipval2lem6 8357  4ipval3 8358  ipid 8359  ipcj 8363  ipipcj 8364  ip0r 8366  ip1cnilem4 8372  ip1cnilem6 8374  sspmval 8388  sspival 8393  lnoval 8409  islno 8410  lnolin 8411  lno0 8413  lnocoi 8414  lnoadd 8415  0lno 8446  nmlnoubi 8452  nmblolbii 8455  blometi 8459  blocnilem 8460  isphg 8472  cnph 8474  isph 8477  phpar2 8478  phpar 8479  ipdiri 8485  ipasslem1 8486  ipasslem2 8487  ipasslem5 8490  ipasslem11 8496  ipassi 8497  ipass 8501  ipassr 8502  ipsubdir 8504  pythi 8506  siilem1 8507  siilem2 8508  siii 8509  sii 8510  sspph 8511  ipblnfi 8512  ajmoi 8515  ubthlem8 8532  ubthlem10 8534  minveclem6 8546  minveclem8 8548  minveclem19 8559  minveclem21 8561  minveclem23 8563  minveclem30 8570  minveclem36 8576  minveceu 8579  htthlem2 8617  htthlem3 8618  sinper 8685  cosper 8686  efimpi 8693  abssinper 8707  sineq0 8708  efifolem2 8718  efifolem3 8719  efifolem6 8722  shftefif1olem 8736  effoi 8740  efper 8742  hvsubvalt 8881  hvaddsubvalt 8897  hvadd23t 8898  hvsub4t 8901  hvaddsub12t 8902  hvpncant 8903  hvaddsubasst 8905  hvsubdistr1t 8911  hvsubdistr2t 8912  hvsubsub4t 8922  hvnegdit 8929  hvaddsub4t 8940  his5t 8948  his2subt 8953  normlem6 8976  normlem9at 8982  norm-iit 9000  norm-iiit 9002  normpyth 9004  normpytht 9007  norm3dift 9012  norm3adift 9015  normpart 9017  polidt 9021  hhph 9040  bcsALT 9041  bcst 9043  hcau2 9050  hhssnv 9129  chocuni 9167  occllem2 9169  projlem7 9187  projlem17 9197  projlem20 9200  projlem22 9202  projlem26 9206  pjthlem8 9221  pjthlem9 9222  omlsilem 9239  pjch 9260  chdmm1t 9443  chdmm3t 9445  chdmm4t 9446  chjasst 9451  chj4t 9453  ledit 9458  spanunt 9463  h1de2b 9472  pjspansnt 9495  spanunsn 9497  hosmvalt 9506  hommvalt 9507  hodmvalt 9508  hfsmvalt 9509  hfmmvalt 9510  homvalt 9513  hfmvalt 9517  cmcmlem 9529  pjoml2t 9549  spansnjt 9587  spansncvt 9593  5oalem1 9594  5oalem2 9595  5oalem3 9596  5oalem5 9598  3oalem2 9603  pjcj 9624  pjadjt 9625  pjaddt 9626  pjsubt 9628  pjmult 9629  pjcjt2 9632  pjopytht 9660  hoaddass 9697  hoaddasst 9703  hoadd23t 9704  hocsubdirt 9706  hoaddid1 9707  honegsub 9717  ho0subt 9718  honegsubt 9720  homco1t 9722  homulasst 9723  hoadddit 9724  hosubnegt 9728  hosubdit 9729  honegsubdit 9731  hosubsub2t 9733  hosub4t 9734  hoaddsubasst 9736  hosubsub4t 9739  adjsymt 9754  eigortht 9759  ellnopt 9779  elhmopt 9795  ellnfnt 9805  adjvalt 9809  cnopct 9832  lnoplt 9833  unopt 9834  unopadjt 9838  unoplint 9839  hmopt 9841  cnfnct 9849  lnfnlt 9850  adjt 9852  adjeqt 9854  hmoplint 9861  bramult 9865  brafnmult 9870  kbpjt 9875  lnopmult 9886  lnopaddmul 9892  lnopsubmul 9894  homco2t 9896  0hmop 9902  0lnfn 9904  hoddit 9910  adj0 9914  lnopm 9920  lnophs 9921  lnopco 9923  lnopeq0lem2 9926  lnopeq0 9927  lnopuni 9932  lnophm 9938  lnophmt 9939  hmopst 9940  hmopmt 9941  hmopcot 9943  nmbdoplb 9944  nmcoplb 9953  lnopcon 9958  lnfnaddmul 9969  lnfnsub 9970  lnfnmult 9972  nmbdfnlb 9973  nmcfnlb 9982  lnfncon 9985  nlelsh 9988  cnlnadjlem2 9996  cnlnadjlem5 9999  cnlnadjlem6 10000  cnlnadjlem9 10003  cnlnssadj 10008  adjlnopt 10014  adjmult 10020  adjaddt 10021  nmopco 10023  adjco 10028  unierr 10032  branmfnt 10033  cnvbravalt 10038  cnvbramult 10043  kbass6t 10049  leopnmidt 10066  hmopidmch 10074  hmopidmpj 10075  pjadjco 10084  pjss2co 10087  pjclem4 10122  pjadj2co 10127  pj3s 10130  pj3cor1 10132  hstel2t 10141  hst1ht 10149  hstlet 10152  hstoht 10154  stjt 10157  st0 10171  stcltrlem1 10198  mdbrt 10216  dmdmdt 10222  ssmd1 10233  ssmd2 10234  mdslmd1lem2 10248  mdslmd3 10254  cvexchlem 10290  atoml2 10305  irredlem3 10314  atcvat3 10318  atabs 10323  sumdmdlem2 10341  cdj1 10355  cdj3lem1 10356  cdj3lem2b 10359  cdj3lem3b 10362  cdj3 10363  ghomgrpilem1 10380  ghomlin 10388  symggrpi 10401  cayleylem2 10405  hmeogrp 10524  mslb1 10600  iscat 10658  cati 10659  1cat 10663  cmpasso 10677  cmpidb 10679

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748  ax-pr 2785

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-xp 3190  df-cnv 3192  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fv 3204  df-opr 3971

Copyright terms: Public domain