Theorem opreq2d 4034

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

Syntax hints:   -> wi 3   = wceq 997  (class class class)co 4021

This theorem is referenced by:  opreq12d 4036  csbopr1g 4046  caoprass 4112  caoprdistr 4117  oaass 4253  odi 4268  omass 4269  nnmsucr 4298  ecoprass 4381  ecoprdi 4382  addasspi 5088  mulasspi 5090  distrpi 5091  addclprlem2 5184  mulclprlem 5186  distrlem4pr 5195  1idpr 5198  prlem934a 5202  prlem936a 5218  prlem936 5220  mulcmpblnrlem 5247  ssgt0sr 5282  supsrlem4 5293  supsr 5296  mulcnsr 5319  ax1id 5347  axcnre 5351  add23 5402  add42 5404  cnegex 5413  negsub 5447  addsubass 5448  subneg 5459  pncan 5462  mul23 5484  muladd 5486  subdi 5492  mul2neg 5519  negdi 5520  negsubdi 5522  submul2 5525  subsub2 5526  subsub4 5529  sub23 5530  nnncan 5531  nppcan2 5535  addsub4 5538  sub4 5541  mulsub 5542  pnncan 5545  divreczi 5800  divrec 5801  divassOLD 5803  divass 5804  divdir 5813  divdirOLD 5814  divsubdir 5832  divsubdirOLD 5833  recrec 5834  divmul24 5841  divadddiv 5842  divdivdiv 5843  divcan6 5849  divdivmul 5853  conjmul 5855  nnmulcl 6001  flhalf 6358  quoremz 6363  quoremnn0 6365  modval 6372  modfrac 6374  flmodOLD 6375  modcyc 6376  modcycOLD 6377  modcyc2 6378  modcyc2OLD 6379  icoshftf1olem 6436  seq1val 6571  seq1suclem 6575  seq1m1 6578  ser1p1i 6595  shftcan1 6613  seq1shftid 6615  seq0fval 6624  seqzfval 6626  seqzp1 6637  seqzm1 6638  seq0p1 6640  seqzval2 6642  ser0p1i 6656  expval 6659  expp1 6663  expm1 6672  recexp 6684  expadd 6685  expmul 6686  expsub 6687  divexp 6688  expordi 6689  subsq2 6732  binom2 6739  bernneq 6741  discrlem2 6747  discrlem3 6748  discrlem 6749  nn0opthi 6756  sqrmuli 6795  sqr2irrlem2 6815  sqr2irrlem3 6816  sqr2irrlem5 6818  crui 6827  cru 6828  crreczi 6831  creur 6832  creui 6833  replim 6851  cjval 6853  imre 6863  reim0b 6865  rereb 6866  mulre 6867  readd 6895  resub 6896  imadd 6898  imsub 6899  cjadd 6902  cjmul 6903  addcj 6905  cjsub 6906  recj 6908  cj11 6920  absneg 6922  abscj 6924  abs00i 6932  sqabsadd 6938  sqabssub 6939  absmul 6948  absdiv 6950  absre 6956  absresq 6957  recvalzi 6977  cjdivi 6978  cjdiv 6979  absmax 6987  abstri 6988  recan 6995  abslem2 6999  cau2i 7003  ser1absdiflem 7019  facp1 7026  facnn2 7029  faclbnd 7035  faclbnd4lem1 7038  faclbnd4lem2 7039  faclbnd4lem3 7040  faclbnd4lem4 7041  faclbnd6 7044  bcval 7048  bccmpl 7052  bcn0 7053  bcnn 7054  bcnp11 7055  bcnp1n 7056  bcpasc2 7058  bcpasci 7059  bcpasc 7060  sumeq2 7075  fsump1slem 7102  fsum1ps 7108  fsum3 7114  fsum4 7115  fsumrev 7119  fsummulc1 7123  fsumcons 7128  fsumabs 7133  ser1ser0i 7138  serz1p 7142  serzmulc1 7147  serzmulci 7148  serzrelem 7151  binomlem1 7156  binomlem2 7157  binomlem3 7158  binomlem4 7159  binomlem5 7160  binomlem6 7161  binomi 7162  binom1pi 7163  bcxmas 7166  climaddc1 7208  climsub 7220  caucvgi 7253  caucvg3ai 7254  caucvg3lem 7256  caucvg3i 7257  caucvg3 7258  serzf0i 7259  ser1f0i 7260  ser1consti 7261  ser1cmp2i 7267  cvgcmp2lem 7270  cvgcmp2i 7271  cvgcmp2ci 7273  cvgcmp3cei 7277  cvgcmp3cetlem1 7278  cvgcmp3cetlem2 7279  isummulc1 7302  isummulc1iALT 7303  isummulc1ai 7304  infcvglem2 7312  infcvgi 7314  arisumi 7316  geoseri 7324  geolimilem 7325  geolimi 7326  geolim 7327  geolim1 7329  georeclim 7330  geoisumr 7333  geoisum1c 7335  0.999... 7336  cvgratlem1ALT 7337  cvgratlem3ALT 7339  cvgratlem1 7340  cvgratlem3 7342  cvgratlem4 7343  cvgratlem5 7344  fsum0diaglem2 7347  fsum0diag 7348  fsum0diag2 7349  fsum0diag4 7351  efcltlem1 7394  efcltlem2 7395  efseq1ex 7396  ef0lem 7400  erelem2 7410  erelem3 7411  ege2lem2 7418  ege2le3lem2 7419  efaddlem6 7433  efaddlem17 7444  efadd 7457  efsub 7461  efexp 7462  eftlex 7468  ef1tllem 7471  ef01tllem1 7473  ef01tllem2 7474  ef01tllem2OLD 7475  eirrlem2 7480  eirrlem5 7483  eflegeo 7507  efcnlem4 7513  resinval 7524  recosval 7525  efi4p 7526  efival 7538  efmival 7539  efeul 7540  sinadd 7544  cosadd 7545  sinsub 7546  cossub 7547  sincossq 7552  sin2t 7553  cos2t 7554  cos2tsin 7555  sin01bndlem3 7561  cos01bndlem3 7563  demoivre 7576  acdc3lem 7578  acdc2lem2 7581  acdc2 7582  acdc5lem2 7584  acdc5 7585  acdclem 7586  ruclem4 7605  ruclem32 7633  cnfval 7841  cnpfval 7842  mettri2 7898  mettri4 7899  metsym 7901  mettri3 7903  metxpdval 7914  metxplem4 7918  metxp 7919  tgioolem 7999  iscau3 8023  iscau4 8025  opr1cn 8063  bcthlem1 8084  bcthlem17 8100  bcthlem20 8103  isgrp 8126  grpass 8132  grpidinvlem2 8134  grpinvid2 8157  isgrp2i 8160  grpinvop 8164  grpdivfval 8165  grpdivval 8166  grpdivinv 8167  grpdivdiv 8171  grpmuldivass 8172  grppncan 8174  grpnpcan 8175  grppnpcan2 8176  abl23 8188  abldivdiv4 8193  abldiv23 8194  ablnnncan 8195  issubgi 8206  grpsn 8208  ablmul 8215  ghgrpilem1 8217  ghgrpilem4 8220  isring 8225  ringi 8226  ringdi 8230  ringdir 8231  ringass 8232  ringsn 8247  vci 8251  vcdi 8255  vcdir 8256  vcass 8257  vcsubdir 8259  vcz 8273  vcm 8274  vcrinv 8275  vcnegsubdi2 8278  vcsub4 8279  isvclem 8280  vcoprne 8282  isnvlem 8313  nvi 8317  nvmval 8347  nvmfval 8348  nvmdi 8354  nvrinv 8357  nvsubadd 8359  nvaddsub4 8365  nvnncan 8367  nvs 8374  nvdif 8377  nvpi 8378  nvtri 8382  nvmtri 8383  nvabs 8385  nvge0 8386  cnnvm 8397  nvnd 8403  imsmetlem 8407  ipfval 8436  ipval 8437  ipval2lem3 8439  ipval2 8441  4ipval2 8442  ipval3 8443  ipval2lem6 8445  4ipval3 8446  ipid 8447  ipcj 8451  ipipcj 8452  ip0r 8454  ip1cnilem4 8460  ip1cnilem6 8462  sspmval 8476  sspival 8481  lnoval 8497  islno 8498  lnolin 8499  lno0 8501  lnocoi 8502  lnoadd 8503  0lno 8534  nmlnoubi 8540  nmblolbii 8543  blometi 8547  blocnilem 8548  isphg 8560  cnph 8562  isph 8565  phpar2 8566  phpar 8567  ipdiri 8573  ipasslem1 8574  ipasslem2 8575  ipasslem5 8578  ipasslem11 8584  ipassi 8585  ipass 8589  ipassr 8590  ipsubdir 8592  pythi 8594  siilem1 8595  siilem2 8596  siii 8597  sii 8598  sspph 8599  ipblnfi 8600  ajmoi 8603  ubthlem8 8620  ubthlem10 8622  minveclem6 8634  minveclem8 8636  minveclem19 8647  minveclem21 8649  minveclem23 8651  minveclem30 8658  minveclem36 8664  minveceu 8667  htthlem2 8705  htthlem3 8706  sinper 8773  cosper 8774  efimpi 8781  abssinper 8795  sineq0 8796  efifolem2 8806  efifolem3 8807  efifolem6 8810  shftefif1olem 8824  effoi 8828  efper 8830  hvsubval 8969  hvaddsubval 8985  hvadd23 8986  hvsub4 8989  hvaddsub12 8990  hvpncan 8991  hvaddsubass 8993  hvsubdistr1 8999  hvsubdistr2 9000  hvsubsub4 9010  hvnegdi 9017  hvaddsub4 9028  his5 9036  his2sub 9041  normlem6 9064  normlem9at 9070  norm-ii 9088  norm-iii 9090  normpythi 9092  normpyth 9095  norm3dif 9100  norm3adifi 9103  normpar 9105  polid 9109  hhph 9128  bcsiALT 9129  bcs 9131  hcau2 9138  hhssnv 9217  chocunii 9255  occllem2 9257  projlem7 9275  projlem17 9285  projlem20 9288  projlem22 9290  projlem26 9294  pjthlem8 9309  pjthlem9 9310  omlsilem 9327  pjchi 9348  chdmm1 9531  chdmm3 9533  chdmm4 9534  chjass 9539  chj4 9541  ledi 9546  spanun 9551  h1de2bi 9560  pjspansn 9583  spanunsni 9585  hosmval 9594  hommval 9595  hodmval 9596  hfsmval 9597  hfmmval 9598  homval 9601  hfmval 9605  cmcmlem 9617  pjoml2 9637  spansnj 9675  spansncv 9681  5oalem1 9682  5oalem2 9683  5oalem3 9684  5oalem5 9686  3oalem2 9691  pjcji 9712  pjadji 9713  pjaddi 9714  pjsubi 9716  pjmuli 9717  pjcjt2 9720  pjopyth 9748  hoaddassi 9785  hoaddass 9791  hoadd23 9792  hocsubdir 9794  hoaddid1i 9795  honegsubi 9805  ho0sub 9806  honegsub 9808  homco1 9810  homulass 9811  hoadddi 9812  hosubneg 9816  hosubdi 9817  honegsubdi 9819  hosubsub2 9821  hosub4 9822  hoaddsubass 9824  hosubsub4 9827  adjsym 9842  eigorth 9847  ellnop 9867  elhmop 9883  ellnfn 9893  adjval 9897  cnopc 9920  lnopl 9921  unop 9922  unopadj 9926  unoplin 9927  hmop 9929  cnfnc 9937  lnfnl 9938  adj1 9940  adjeq 9942  hmoplin 9949  bramul 9953  brafnmul 9958  kbpj 9963  lnopmul 9974  lnopaddmuli 9980  lnopsubmuli 9982  homco2 9984  0hmop 9990  0lnfn 9992  hoddi 9998  adj0 10002  lnopmi 10008  lnophsi 10009  lnopcoi 10011  lnopeq0lem2 10014  lnopeq0i 10015  lnopunii 10020  lnophmi 10026  lnophm 10027  hmops 10028  hmopm 10029  hmopco 10031  nmbdoplbi 10032  nmcoplbi 10041  lnopconi 10046  lnfnaddmuli 10057  lnfnsubi 10058  lnfnmul 10060  nmbdfnlbi 10061  nmcfnlbi 10070  lnfnconi 10073  nlelshi 10076  cnlnadjlem2 10084  cnlnadjlem5 10087  cnlnadjlem6 10088  cnlnadjlem9 10091  cnlnssadj 10096  adjlnop 10102  adjmul 10108  adjadd 10109  nmopcoi 10111  adjcoi 10116  unierri 10120  branmfn 10121  cnvbraval 10126  cnvbramul 10131  kbass6 10137  leopnmid 10154  hmopidmchi 10162  hmopidmpji 10163  pjadjcoi 10172  pjss2coi 10175  pjclem4 10211  pjadj2coi 10216  pj3si 10219  pj3cor1i 10221  hstel2 10230  hst1h 10238  hstle 10241  hstoh 10243  stj 10246  st0 10260  stcltrlem1 10287  mdbr 10305  dmdmd 10311  ssmd1 10322  ssmd2 10323  mdslmd1lem2 10337  mdslmd3i 10343  cvexchlem 10379  atoml2i 10394  irredlem3 10403  atcvat3i 10407  atabsi 10412  sumdmdlem2 10430  cdj1i 10444  cdj3lem1 10445  cdj3lem2b 10448  cdj3lem3b 10451  cdj3i 10452  ghomgrpilem1 10470  ghomlin 10478  symggrpi 10491  cayleylem2 10495  vri 10583  hmeogrp 10632  mslb1 10711  iscat 10769  cati 10770  1cat 10774  cmpasso 10788  cmpidb 10790

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-xp 3241  df-cnv 3243  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fv 3255  df-opr 4023

Copyright terms: Public domain