Theorem opreq1d 3975

Description: Equality deduction for operation value.

Hypothesis

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

Assertion

Ref	Expression
opreq1d	|- (ph -> (AFC) = (BFC))

Proof of Theorem opreq1d

Step	Hyp	Ref	Expression
1		opreq1d.1	. 2 |- (ph -> A = B)
2		opreq1 3968	. 2 |- (A = B -> (AFC) = (BFC))
3	1, 2	syl 10	1 |- (ph -> (AFC) = (BFC))

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

This theorem is referenced by:  opreq12d 3978  csbopr2g 3989  caoprass 4054  caoprdistr 4059  om1 4176  oe1 4178  omass 4211  nnmsucr 4240  nneob 4255  ecoprass 4320  ecoprdi 4321  addasspi 5023  mulasspi 5025  addclprlem1 5118  prlem934a 5137  reclem3pr 5158  mulcmpblnrlem 5182  1idsr 5207  pn0sr 5210  recexsrlem 5212  mulgt0sr 5214  ssgt0sr 5217  supsrlem2 5226  ax1id 5282  axcnre 5286  add12t 5336  add4t 5338  cnegext 5348  addsubt 5384  2addsubt 5389  pncan2t 5398  npncant 5400  nppcant 5401  mul12t 5418  mul4t 5420  muladd11t 5422  ine0 5434  mulneg1t 5451  mul2negt 5454  negdit 5455  nnncan1t 5467  nncant 5469  pnpcant 5478  ppncant 5481  recext 5684  divcan1t 5724  divcan1tOLD 5725  div23t 5742  div13t 5743  divdirt 5750  divdirtOLD 5751  divcan3t 5760  divcan3tOLD 5761  divcan4t 5762  divcan4tOLD 5763  divsubdirtOLD 5775  divmuldivt 5780  divcan5t 5781  divmul13t 5782  divadddivt 5784  divdivdivt 5785  divdiv23t 5792  divdivmult 5795  conjmult 5797  lt2mul2divt 5872  nnsub 5956  nndivtrt 5960  2halvest 6039  halfaddsubt 6041  nneo 6197  nneot 6198  zeot 6199  zneo 6200  uzindOLD 6208  flleltt 6228  quoremOLD 6252  qrecclt 6273  om2uzsuc 6296  uzrdgsuc 6304  seq1lem1 6309  seq1rval 6311  seq1suclem 6316  shftcan1t 6354  icoshftf1olem 6410  seq0fval 6535  seqzfval 6537  seqzp1 6548  seq0p1 6551  dfseq0 6563  expp1t 6574  divexpt 6599  sqvalt 6609  subsqt 6642  subsq2t 6643  binom2t 6650  bernneq2 6653  discrlem2 6657  discrlem3 6658  discrlem 6659  nn0opth 6666  nn0opth2t 6668  sqrlem21 6693  sqrmul 6705  sqsqrt 6723  sqr2irrlem2 6725  replimt 6761  mulretOLD 6777  cjmulvalt 6802  readdt 6805  imaddt 6808  cjaddt 6812  cjmult 6813  recjt 6818  imcjt 6819  absvalsqt 6835  absval2t 6852  absreimsqt 6856  absmult 6858  absdivt 6860  cjdivt 6889  absmaxt 6897  abstrit 6898  ser1absdiflem 6929  ser1absdif 6930  facp1t 6936  facdivt 6942  facndivt 6943  faclbnd 6945  faclbnd2 6946  faclbnd3 6947  faclbnd4lem2 6949  faclbnd4lem4 6951  bcvalt 6958  bccmplt 6962  bcpasc2t 6968  bcpasc 6969  bcpasct 6970  clim 6977  dffsum 6998  fsum1ps 7018  fsum1p 7019  fsumsplit 7020  fsum0split 7021  fsum2 7023  csbfsumlem 7026  fsumrev 7029  fsumconst 7038  ser1ser0 7048  binomlem1 7066  binomlem2 7067  binomlem3 7068  binomlem4 7069  binomlem5 7070  binomlem6 7071  binom 7072  binom1p 7073  bcxmas 7076  clmnns 7084  climfnn 7092  climshft 7104  climres 7105  climrecl 7110  climge0 7112  climaddlem3 7116  climmullem8 7127  climmulc2 7129  climsubc2 7131  iserzex 7146  climabslem 7148  climubi 7153  climcau 7156  caucvg 7163  caucvg3t 7168  serzf0 7169  ser1f0 7170  ser1clim0 7173  dfisum 7191  fnsmntlem 7225  fnsmnt 7226  geoser 7234  geolimilem 7235  geolimi 7236  geoisumr 7243  cvgratlem1ALT 7247  cvgratlem2ALT 7248  cvgratlem1 7250  cvgratlem2 7251  cvgratlem3 7252  fsum0diaglem2 7257  fsum0diag 7258  fsum0diag2 7259  fsum0diag4 7261  ivthlem8 7288  efcltlem1 7304  efcltlem2 7305  efseq1ex 7306  efvalt 7308  eval 7309  ef0lem 7310  erelem6 7324  efaddlem5 7342  efaddlem6 7343  efaddlem16 7353  efaddt 7367  eftlext 7378  ef1tllem 7381  ef1tlub 7382  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  ef01tlub 7386  absef01tlub 7388  eirrlem2 7390  eirrlem5 7393  abspef01tlub 7395  ef4pt 7400  efm1legeot 7418  sinvalt 7429  cosvalt 7430  resinvalt 7433  recosvalt 7434  efi4pt 7435  resin4pt 7436  recos4pt 7437  sinnegt 7442  cosnegt 7443  efivalt 7447  sinaddt 7453  cosaddt 7454  cos2tt 7463  demoivre 7484  demoivreALT 7485  xpnnen 7499  znnenlem 7501  ruclem4 7513  ruclem32 7541  cnfval 7756  cnpfval 7757  mettri2 7813  mettri4 7814  mettri 7817  metxpdval 7829  metxplem4 7833  metcni 7894  cnmet 7904  ioo2bl 7912  tgioolem 7914  lmbr 7928  lmconst 7934  iscau3 7938  iscau4 7940  lmbrnns 7942  lmcvgnns 7943  lmfexlem3 7958  lmle 7960  metelcls 7965  metcnp4lem2 7969  metcnp4 7970  xplmi 7973  xplm 7975  opr2cn 7979  opr1scn 7980  iscms2lem4 7992  lmcau 7996  bcthlem2 8000  bcthlem15 8013  bcthlem16 8014  bcthlem18 8016  bcthlem24 8022  bcthlem26 8024  isgrp 8041  grpass 8047  grpinvid1 8072  grplcan 8075  isgrp2i 8076  grpasscan1 8077  grpinvop 8080  grpinvdiv 8084  grpnpcan 8091  grppnpcan2 8092  grpnpncan 8094  abl4 8105  ablmuldiv 8107  ablnncan 8112  ablnnncan1 8113  issubgi 8122  grpsn 8124  ablmul 8131  ghgrpilem1 8133  ghgrpilem4 8136  isring 8141  ringi 8142  ringdi 8146  ringdir 8147  ringass 8148  ringsn 8163  vcdi 8171  vcdir 8172  vcass 8173  vcsubdir 8175  vc0 8188  vcz 8189  vcm 8190  vclinv 8192  nvadd12 8242  nvscom 8250  nvmul0or 8272  nvlinv 8274  nvpncan2 8276  nvpncan 8277  nvnncan 8283  nvs 8290  nvsge0 8291  nvtri 8298  nvge0 8302  imsmetlem 8323  nmcn 8339  ipfval 8352  ipval 8353  ipval2lem3 8355  ipval2 8357  ipval3 8359  ipval2lem6 8361  ipid 8363  ipcj 8367  ip0r 8370  ip1cnilem4 8376  ip1cnilem6 8378  sspival 8397  lnolin 8415  lnomul 8421  nmblolbi 8460  isphg 8476  cnph 8478  isph 8481  phpar2 8482  phpar 8483  ipdiri 8489  ipasslem1 8490  ipasslem2 8491  ipasslem3 8492  ipasslem4 8493  ipasslem5 8494  ipasslem6 8495  ipasslem8 8497  ipasslem9 8498  ipasslem11 8500  ipassi 8501  ipdir 8502  ipass 8505  ipassr2 8507  ipsubdir 8508  sii 8514  sspph 8515  ubthlem8 8536  minveclem18 8562  minveclem21 8565  minveclem27 8571  minveclem31 8575  minveclem33 8577  minveclem36 8580  minveclem38 8582  htthlem2 8621  htthlem4 8623  sinkpi 8697  abssinper 8712  sineq0 8713  efifolem3 8724  eff1lem 8743  eff1i 8744  explogt 8772  reexplogt 8773  relogexpt 8774  hvmul0t 8893  hvmul0ort 8894  hvsubidt 8895  hvm1negt 8901  hvadd12t 8904  hvadd4t 8905  hvpncan2t 8909  hvmulcomt 8912  hvsubdistr2t 8917  hvsubsub4t 8927  hvaddsub4t 8945  his52t 8954  hiassdit 8957  his2subt 8958  normlem6 8981  normlem7tALT 8985  bcseq 8986  normlem9at 8987  normsqt 9001  norm-iit 9005  norm-iiit 9007  normpytht 9012  norm3dift 9017  norm3dif2t 9018  norm3adift 9020  normpart 9022  polidt 9026  hhph 9045  bcst 9048  hcau2 9055  hlim 9056  hlim2 9060  hlim0 9105  hlimcaui 9106  norm1t 9121  chocuni 9172  occllem2 9174  occllem3 9175  occllem5 9177  occllem6 9178  projlem7 9192  projlem22 9207  projlem23 9208  projlem25 9210  projlem26 9211  pjthlem7 9225  pjthlem8 9226  pjthlem9 9227  chdmm1t 9448  chdmm2t 9449  chjasst 9456  chj12t 9457  ledit 9463  spanunt 9468  h1de2b 9477  elspansn2t 9490  spansncol 9491  normcant 9499  pjspansnt 9500  spanunsn 9502  h1datom 9504  hosmvalt 9511  hodmvalt 9513  hfsmvalt 9514  cmbr3t 9551  pjoml3t 9555  fh2t 9562  osumlem2 9579  5oalem2 9600  3oalem2 9608  pjadjt 9630  pjaddt 9631  pjinormt 9632  pjsubt 9633  pjige0t 9636  pjcjt2 9637  pjds3 9658  pjopytht 9665  pjpytht 9670  mayete3 9673  hoaddass 9702  hoaddasst 9708  hoadd4t 9710  hocsubdirt 9711  homul12t 9731  hoaddsubt 9742  adjmo 9758  adjsymt 9759  eigpos 9762  eigortht 9764  elhmopt 9800  eigvalvalt 9823  lnoplt 9838  unopt 9839  hmopt 9846  lnfnlt 9855  adjt 9857  adjeqt 9859  hmopadj2t 9865  bralnfnt 9872  kbvalt 9876  kbvalvalt 9878  kbmult 9879  kbpjt 9880  eigvalt 9884  eigvect 9886  lnop0t 9890  lnopadd 9895  lnopmulsub 9900  0hmop 9907  hoddit 9915  adj0 9919  lnopeq0lem2 9931  lnopeq0 9932  lnopeq 9933  lnopeqt 9934  lnopuni 9937  lnophm 9943  hmopst 9945  hmopmt 9946  hmopcot 9948  nmbdoplb 9949  nmbdoplbt 9950  nmcopexlem3 9953  nmcopexlem5 9955  nmcoplb 9958  nmcoplbt 9960  nmophm 9961  lnfnadd 9972  nmbdfnlb 9978  nmbdfnlbt 9979  nmcfnexlem3 9982  nmcfnexlem5 9984  nmcfnlb 9987  nmcfnlbt 9989  nlelch 9994  cnlnadjlem1 10000  cnlnadjlem2 10001  cnlnadjlem5 10004  cnlnadjeut 10011  cnlnssadj 10013  adjmult 10025  adjaddt 10026  nmopco 10028  adjco 10033  unierr 10037  cnvbramult 10048  kbass1t 10049  kbass5t 10053  kbass6t 10054  leopg 10055  leop2t 10057  leop3t 10058  leoppost 10059  leoprf2t 10060  leoprft 10061  leopsqt 10062  idleop 10064  leopaddt 10065  leopmulit 10066  leopmult 10067  leopnmidt 10071  nmopleidt 10072  hmopidmchlem 10078  hmopidmch 10079  pjadjco 10089  pjsspos 10100  pjssdif2 10102  pjssdif1 10103  pjclem4 10127  pjadj2co 10132  pj3s 10135  pj3cor1 10137  hstel2t 10146  hstnmoct 10150  hst1ht 10154  hstpytht 10156  stjt 10162  strlem1 10177  strlem2 10178  strlem3a 10179  strlem4 10181  golem1 10198  mdbr3 10224  mdbr4 10225  dmdbrt 10226  dmdmdt 10227  dmdit 10229  dmdbr3 10232  dmdbr4 10233  dmdi4 10234  dmdbr5 10235  mdslmd1lem1 10252  mdslmd1lem3 10254  mdslmd1lem4 10255  sumdmdlem2 10346  cdj3lem1 10361  cdj3lem2b 10364  cdj3lem3b 10367  cdj3 10368  abs2sqlet 10374  abs2sqltt 10375  ghomgrpilem1 10385  ghomlin 10393  symggrpi 10406  cayleylem2 10410  hmeogrp 10538  mslb1 10629  2wsms 10630  iscat 10687  cati 10688  1cat 10692  cmpasso 10706  cmpida 10707  idmon 10745

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 2703  ax-pow 2742  ax-pr 2779

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 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-xp 3184  df-cnv 3186  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fv 3198  df-opr 3965

Copyright terms: Public domain