Theorem opreq1d 4033

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 4026	. 2 |- (A = B -> (AFC) = (BFC))
3	1, 2	syl 10	1 |- (ph -> (AFC) = (BFC))

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

This theorem is referenced by:  opreq12d 4036  csbopr2g 4047  caoprass 4112  caoprdistr 4117  om1 4234  oe1 4236  omass 4269  nnmsucr 4298  nneob 4313  ecoprass 4381  ecoprdi 4382  addasspi 5088  mulasspi 5090  addclprlem1 5183  prlem934a 5202  reclem3pr 5223  mulcmpblnrlem 5247  1idsr 5272  pn0sr 5275  recexsrlem 5277  mulgt0sr 5279  ssgt0sr 5282  supsrlem2 5291  ax1id 5347  axcnre 5351  add12 5401  add4 5403  cnegex 5413  addsub 5449  2addsub 5454  pncan2 5463  npncan 5465  nppcan 5466  mul12 5483  mul4 5485  muladd11 5487  ine0 5499  mulneg1 5516  mul2neg 5519  negdi 5520  nnncan1 5532  nncan 5534  pnpcan 5543  ppncan 5546  recex 5749  divcan1 5788  div23 5805  div13 5806  divdir 5813  divdirOLD 5814  divcan3 5819  divcan4 5820  divsubdir 5832  divsubdirOLD 5833  divmuldiv 5838  divcan5 5839  divmul13 5840  divadddiv 5842  divdivdiv 5843  divdiv23 5850  divdivmul 5853  conjmul 5855  lt2mul2div 5931  nnsubi 6017  nndivtr 6021  2halves 6100  halfaddsub 6102  nneoi 6282  nneo 6283  zeo 6284  zneo 6285  uzindOLD 6293  qreccl 6325  fllelt 6339  fldiv 6368  modcyc2 6378  modcyc2OLD 6379  icoshftf1olem 6436  om2uzsuci 6554  uzrdgsuci 6563  seq1lem1 6568  seq1rval 6570  seq1suclem 6575  shftcan1 6613  seq0fval 6624  seqzfval 6626  seqzp1 6637  seq0p1 6640  dfseq0 6652  expp1 6663  divexp 6688  sqval 6698  subsq 6731  subsq2 6732  binom2 6739  bernneq2 6742  discrlem2 6747  discrlem3 6748  discrlem 6749  nn0opthi 6756  nn0opth2 6758  sqrlem21 6783  sqrmuli 6795  sqsqr 6813  sqr2irrlem2 6815  replim 6851  cjmulval 6892  readd 6895  imadd 6898  cjadd 6902  cjmul 6903  recj 6908  imcj 6909  absvalsq 6925  absval2 6942  absreimsq 6946  absmul 6948  absdiv 6950  cjdiv 6979  absmax 6987  abstri 6988  ser1absdiflem 7019  ser1absdifi 7020  facp1 7026  facdiv 7032  facndiv 7033  faclbnd 7035  faclbnd2 7036  faclbnd3 7037  faclbnd4lem2 7039  faclbnd4lem4 7041  bcval 7048  bccmpl 7052  bcpasc2 7058  bcpasci 7059  bcpasc 7060  clim 7067  dffsum 7088  fsum1ps 7108  fsum1p 7109  fsumspl 7110  fsum0spl 7111  fsum2 7113  csbfsumlem 7116  fsumrev 7119  fsumcons 7128  ser1ser0i 7138  binomlem1 7156  binomlem2 7157  binomlem3 7158  binomlem4 7159  binomlem5 7160  binomlem6 7161  binomi 7162  binom1pi 7163  bcxmas 7166  clmnnsi 7174  climfnn 7182  climshfti 7194  climresi 7195  climrecl 7200  climge0 7202  climaddlem3 7206  climmullem8 7217  climmulc2 7219  climsubc2 7221  iserzexi 7236  climabslem 7238  climubii 7243  climcaui 7246  caucvgi 7253  caucvg3 7258  serzf0i 7259  ser1f0i 7260  ser1clim0 7263  dfisum 7281  arisumilem 7315  arisumi 7316  geoseri 7324  geolimilem 7325  geolimi 7326  geoisumr 7333  cvgratlem1ALT 7337  cvgratlem2ALT 7338  cvgratlem1 7340  cvgratlem2 7341  cvgratlem3 7342  fsum0diaglem2 7347  fsum0diag 7348  fsum0diag2 7349  fsum0diag4 7351  ivthlem8 7378  efcltlem1 7394  efcltlem2 7395  efseq1ex 7396  efval 7398  eval 7399  ef0lem 7400  erelem6 7414  efaddlem5 7432  efaddlem6 7433  efaddlem16 7443  efadd 7457  eftlex 7468  ef1tllem 7471  ef1tlubi 7472  ef01tllem1 7473  ef01tllem2 7474  ef01tllem2OLD 7475  ef01tlubi 7476  absef01tlubi 7478  eirrlem2 7480  eirrlem5 7483  abspef01tlubi 7486  ef4p 7491  efm1legeo 7509  sinval 7520  cosval 7521  resinval 7524  recosval 7525  efi4p 7526  resin4p 7527  recos4p 7528  sinneg 7533  cosneg 7534  efival 7538  sinadd 7544  cosadd 7545  cos2t 7554  cos2tsin 7555  demoivre 7576  demoivreALT 7577  xpnnen 7591  znnenlem 7593  ruclem4 7605  ruclem32 7633  cnfval 7841  cnpfval 7842  mettri2 7898  mettri4 7899  mettri 7902  metxpdval 7914  metxplem4 7918  metcni 7979  cnmet 7989  ioo2bl 7997  tgioolem 7999  lmbr 8013  lmconst 8019  iscau3 8023  iscau4 8025  lmbrnns 8027  lmcvgnns 8028  lmfexlem3 8043  lmle 8045  metelcls 8050  metcnp4lem2 8054  metcnp4 8055  xplmi 8058  xplm 8060  opr2cn 8064  opr1scn 8065  iscms2lem4 8077  lmcau 8081  bcthlem2 8085  bcthlem15 8098  bcthlem16 8099  bcthlem18 8101  bcthlem24 8107  bcthlem26 8109  isgrp 8126  grpass 8132  grpinvid1 8156  grplcan 8159  isgrp2i 8160  grpasscan1 8161  grpinvop 8164  grpinvdiv 8168  grpnpcan 8175  grppnpcan2 8176  grpnpncan 8178  abl4 8189  ablmuldiv 8191  ablnncan 8196  ablnnncan1 8197  issubgi 8206  grpsn 8208  ablmul 8215  ghgrpilem1 8217  ghgrpilem4 8220  isring 8225  ringi 8226  ringdi 8230  ringdir 8231  ringass 8232  ringsn 8247  vcdi 8255  vcdir 8256  vcass 8257  vcsubdir 8259  vc0 8272  vcz 8273  vcm 8274  vclinv 8276  nvadd12 8326  nvscom 8334  nvmul0or 8356  nvlinv 8358  nvpncan2 8360  nvpncan 8361  nvnncan 8367  nvs 8374  nvsge0 8375  nvtri 8382  nvge0 8386  imsmetlem 8407  nmcn 8423  ipfval 8436  ipval 8437  ipval2lem3 8439  ipval2 8441  ipval3 8443  ipval2lem6 8445  ipid 8447  ipcj 8451  ip0r 8454  ip1cnilem4 8460  ip1cnilem6 8462  sspival 8481  lnolin 8499  lnomul 8505  nmblolbi 8544  isphg 8560  cnph 8562  isph 8565  phpar2 8566  phpar 8567  ipdiri 8573  ipasslem1 8574  ipasslem2 8575  ipasslem3 8576  ipasslem4 8577  ipasslem5 8578  ipasslem6 8579  ipasslem8 8581  ipasslem9 8582  ipasslem11 8584  ipassi 8585  ipdir 8586  ipass 8589  ipassr2 8591  ipsubdir 8592  sii 8598  sspph 8599  ubthlem8 8620  minveclem18 8646  minveclem21 8649  minveclem27 8655  minveclem31 8659  minveclem33 8661  minveclem36 8664  minveclem38 8666  htthlem2 8705  htthlem4 8707  sinkpi 8780  abssinper 8795  sineq0 8796  efifolem3 8807  eff1lem 8826  eff1i 8827  explog 8855  reexplog 8856  relogexp 8857  hvmul0 8976  hvmul0or 8977  hvsubid 8978  hvm1neg 8984  hvadd12 8987  hvadd4 8988  hvpncan2 8992  hvmulcom 8995  hvsubdistr2 9000  hvsubsub4 9010  hvaddsub4 9028  his52 9037  hiassdi 9040  his2sub 9041  normlem6 9064  normlem7tALT 9068  bcseqi 9069  normlem9at 9070  normsq 9084  norm-ii 9088  norm-iii 9090  normpyth 9095  norm3dif 9100  norm3dif2 9101  norm3adifi 9103  normpar 9105  polid 9109  hhph 9128  bcs 9131  hcau2 9138  hlimi 9139  hlim2 9143  hlim0 9188  hlimcauii 9189  norm1 9204  chocunii 9255  occllem2 9257  occllem3 9258  occllem5 9260  occllem6 9261  projlem7 9275  projlem22 9290  projlem23 9291  projlem25 9293  projlem26 9294  pjthlem7 9308  pjthlem8 9309  pjthlem9 9310  chdmm1 9531  chdmm2 9532  chjass 9539  chj12 9540  ledi 9546  spanun 9551  h1de2bi 9560  elspansn2 9573  spansncol 9574  normcan 9582  pjspansn 9583  spanunsni 9585  h1datomi 9587  hosmval 9594  hodmval 9596  hfsmval 9597  cmbr3 9634  pjoml3 9638  fh2 9645  osumlem2 9662  5oalem2 9683  3oalem2 9691  pjadji 9713  pjaddi 9714  pjinormi 9715  pjsubi 9716  pjige0 9719  pjcjt2 9720  pjds3i 9741  pjopyth 9748  pjpyth 9753  mayete3i 9756  hoaddassi 9785  hoaddass 9791  hoadd4 9793  hocsubdir 9794  homul12 9814  hoaddsub 9825  adjmo 9841  adjsym 9842  eigposi 9845  eigorth 9847  elhmop 9883  eigvalval 9906  lnopl 9921  unop 9922  hmop 9929  lnfnl 9938  adj1 9940  adjeq 9942  hmopadj2 9948  bralnfn 9955  kbval 9959  kbvalval 9961  kbmul 9962  kbpj 9963  eigval1 9967  eigvec1 9969  lnop0 9973  lnopaddi 9978  lnopmulsubi 9983  0hmop 9990  hoddi 9998  adj0 10002  lnopeq0lem2 10014  lnopeq0i 10015  lnopeqi 10016  lnopeq 10017  lnopunii 10020  lnophmi 10026  hmops 10028  hmopm 10029  hmopco 10031  nmbdoplbi 10032  nmbdoplb 10033  nmcopexlem3 10036  nmcopexlem5 10038  nmcoplbi 10041  nmcoplb 10043  nmophmi 10044  lnfnaddi 10055  nmbdfnlbi 10061  nmbdfnlb 10062  nmcfnexlem3 10065  nmcfnexlem5 10067  nmcfnlbi 10070  nmcfnlb 10072  nlelchi 10077  cnlnadjlem1 10083  cnlnadjlem2 10084  cnlnadjlem5 10087  cnlnadjeu 10094  cnlnssadj 10096  adjmul 10108  adjadd 10109  nmopcoi 10111  adjcoi 10116  unierri 10120  cnvbramul 10131  kbass1 10132  kbass5 10136  kbass6 10137  leopg 10138  leop2 10140  leop3 10141  leoppos 10142  leoprf2 10143  leoprf 10144  leopsq 10145  idleop 10147  leopadd 10148  leopmuli 10149  leopmul 10150  leopnmid 10154  nmopleid 10155  hmopidmchlem 10161  hmopidmchi 10162  pjadjcoi 10172  pjssposi 10183  pjssdif2i 10185  pjssdif1i 10186  pjclem4 10211  pjadj2coi 10216  pj3si 10219  pj3cor1i 10221  hstel2 10230  hstnmoc 10234  hst1h 10238  hstpyth 10240  stj 10246  strlem1 10261  strlem2 10262  strlem3a 10263  strlem4 10265  golem1 10282  mdbr3 10308  mdbr4 10309  dmdbr 10310  dmdmd 10311  dmdi 10313  dmdbr3 10316  dmdbr4 10317  dmdi4 10318  dmdbr5 10319  mdslmd1lem1 10336  mdslmd1lem3 10338  mdslmd1lem4 10339  sumdmdlem2 10430  cdj3lem1 10445  cdj3lem2b 10448  cdj3lem3b 10451  cdj3i 10452  abs2sqlet 10459  abs2sqltt 10460  ghomgrpilem1 10470  ghomlin 10478  symggrpi 10491  cayleylem2 10495  hmeogrp 10632  mslb1 10711  2wsms 10712  iscat 10769  cati 10770  1cat 10774  cmpasso 10788  cmpida 10789  idmon 10827

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