Theorem opreq1d 3960

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

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

This theorem is referenced by:  opreq12d 3963  csbopr2g 3974  caoprass 4040  caoprdistr 4045  om1 4160  oe1 4162  omass 4195  nnmsucr 4224  nneob 4239  ecoprass 4304  ecoprdi 4305  addasspi 4995  mulasspi 4997  addclprlem1 5090  prlem934a 5109  reclem3pr 5130  mulcmpblnrlem 5154  1idsr 5179  pn0sr 5182  recexsrlem 5184  mulgt0sr 5186  ssgt0sr 5189  supsrlem2 5198  ax1id 5254  axcnre 5258  add12t 5308  add4t 5310  cnegext 5320  addsubt 5356  2addsubt 5361  pncan2t 5370  npncant 5372  nppcant 5373  mul12t 5390  mul4t 5392  muladd11t 5394  ine0 5406  mulneg1t 5423  mul2negt 5426  negdit 5427  nnncan1t 5439  nncant 5441  pnpcant 5450  ppncant 5453  recext 5657  divcan1t 5689  div23t 5705  div13t 5706  divdirt 5713  divcan3t 5718  divcan4t 5719  divsubdirt 5731  divmuldivt 5736  divcan5t 5737  divmul13t 5738  divadddivt 5740  divdivdivt 5741  divdiv23t 5748  divdivmult 5751  conjmult 5753  lt2mul2divt 5822  nnsub 5903  nndivtrt 5907  2halvest 5986  halfaddsubt 5988  nneo 6144  nneot 6145  zeot 6146  zneo 6147  zneoOLD 6148  uzindOLD 6156  flleltt 6175  qrecclt 6211  om2uzsuc 6233  uzrdgsuc 6241  seq1lem1 6246  seq1rval 6248  seq1suclem 6253  shftcan1t 6291  icoshftf1olem 6343  seq0fval 6467  seqzfval 6469  seqzp1 6480  seq0p1 6483  dfseq0 6495  expp1t 6506  divexpt 6530  sqvalt 6540  subsqt 6573  subsq2t 6574  binom2t 6581  bernneq2 6584  discrlem2 6587  discrlem3 6588  discrlem 6589  nn0opth 6596  nn0opth2t 6598  sqrlem21 6623  sqrmul 6635  sqsqrt 6653  sqr2irrlem2 6655  replimt 6692  cjmulvalt 6737  readdt 6740  imaddt 6743  cjaddt 6747  cjmult 6748  recjt 6753  imcjt 6754  absvalsqt 6770  absval2t 6787  absreimsqt 6791  absmult 6793  absdivt 6795  cjdivt 6827  abstrit 6835  recant 6842  ser1absdiflem 6866  ser1absdif 6867  facp1t 6873  facdivt 6879  facndivt 6880  faclbnd 6882  faclbnd2 6883  faclbnd3 6884  faclbnd4lem2 6886  faclbnd4lem4 6888  bcvalt 6895  bccmplt 6900  bcpasc2t 6906  bcpasc 6907  bcpasct 6908  clim 6915  dffsum 6936  fsum1ps 6956  fsum1p 6957  fsumsplit 6958  fsum0split 6959  fsum2 6961  csbfsumlem 6964  fsumrev 6967  fsumconst 6976  ser1ser0 6986  binomlem1 7004  binomlem2 7005  binomlem3 7006  binomlem4 7007  binomlem5 7008  binomlem6 7009  binom 7010  binom1p 7011  bcxmas 7014  clmnns 7022  climfnn 7030  climshft 7041  climres 7042  climrecl 7047  climge0 7049  climaddlem3 7052  climmullem8 7063  climmulc2 7065  climsubc2 7067  iserzex 7082  climabslem 7084  climubi 7089  climcau 7092  caucvg 7099  caucvg3a 7100  caucvg3lem 7102  caucvg3t 7104  serzf0 7105  ser1f0 7106  ser1clim0 7109  dfisum 7127  fnsmntlem 7160  fnsmnt 7161  geoser 7169  geolimilem 7170  geolimi 7171  geoisumr 7178  cvgratlem1ALT 7182  cvgratlem2ALT 7183  cvgratlem1 7185  cvgratlem2 7186  cvgratlem3 7187  fsum0diaglem2 7192  fsum0diag 7193  fsum0diag2 7194  fsum0diag4 7196  ivthlem8 7223  ivthlem8OLD 7232  efcltlem1 7246  efcltlem2 7247  efseq1ex 7248  efvalt 7250  eval 7251  ef0lem 7252  erelem6 7266  efaddlem5 7284  efaddlem6 7285  efaddlem16 7295  efaddt 7309  eftlext 7320  ef1tllem 7323  ef1tlub 7324  ef01tllem1 7325  ef01tllem2 7326  ef01tlub 7327  absef01tlub 7329  eirrlem2 7331  eirrlem5 7334  abspef01tlub 7336  ef4pt 7341  efm1legeot 7358  sinvalt 7371  cosvalt 7372  resinvalt 7375  recosvalt 7376  efi4pt 7377  resin4pt 7378  recos4pt 7379  sinnegt 7384  cosnegt 7385  efivalt 7389  sinaddt 7395  cosaddt 7396  cos2tt 7405  demoivre 7426  demoivreALT 7427  xpnnen 7441  znnenlem 7443  znnenlemOLD 7444  ruclem4 7456  ruclem32 7484  cnfval 7696  cnpfval 7697  mettri2 7752  mettri4 7753  mettri 7756  mettriOLD 7757  metxpdval 7769  metxplem4 7773  metcni 7833  cnmet 7843  ioo2bl 7851  tgioolem 7853  lmbr 7866  lmconst 7872  iscau3 7876  lmcvgnns 7879  lmfexlem3 7893  lmle 7895  metelcls 7900  metcnp4lem2 7903  metcnp4 7904  xplmi 7907  xplm 7909  opr2cn 7913  opr1scn 7914  iscms2lem4 7926  lmcau 7930  bcthlem2 7934  bcthlem15 7947  bcthlem16 7948  bcthlem18 7950  bcthlem24 7956  bcthlem26 7958  isgrp 7975  grpass 7981  grpinvid1 8006  grpasscan1OLD 8008  grplcan 8010  isgrp2i 8011  grpasscan1 8012  grpinvop 8015  grpinvdiv 8019  grpnpcan 8026  grppnpcan2 8027  grpnpncan 8029  abl4 8041  ablmuldiv 8044  ablnncan 8049  ablnnncan1 8050  issubgi 8059  grpsn 8061  ablmul 8068  ghgrpilem1 8070  ghgrpilem4 8073  isring 8078  ringi 8079  ringdi 8083  ringdir 8084  ringass 8085  ringsn 8100  vcdi 8108  vcdir 8109  vcass 8110  vcsubdir 8112  vc0 8125  vcz 8126  vcm 8127  vclinv 8129  nvadd12 8182  nvscom 8190  nvmul0or 8212  nvlinv 8214  nvpncan2 8216  nvpncan 8217  nvnncan 8223  nvs 8229  nvsge0 8230  nvtri 8237  nvge0 8241  imsmetlem 8261  nmcn 8274  ipfval 8286  ipval 8287  ipval2lem3 8289  ipval2 8291  ipval3 8293  ipval2lem6 8295  ipid 8297  ipcj 8301  ip0r 8304  ip1cnilem4 8310  ip1cnilem6 8312  sspival 8331  lnolin 8349  lnomul 8354  nmblolbi 8391  isphg 8407  cnph 8409  isph 8412  phpar2 8413  phpar 8414  ipdiri 8420  ipasslem1 8421  ipasslem2 8422  ipasslem3 8423  ipasslem4 8424  ipasslem5 8425  ipasslem6 8426  ipasslem8 8428  ipasslem9 8429  ipasslem11 8431  ipassi 8432  ipdir 8433  ipass 8436  ipassr2 8438  ipsubdir 8439  sii 8445  sspph 8446  ubthlem8 8467  minveclem18 8493  minveclem21 8496  minveclem27 8502  minveclem31 8506  minveclem33 8508  minveclem36 8511  minveclem38 8513  htthlem2 8551  htthlem4 8553  efifolem3 8639  circgrpOLD 8658  eff1lem 8664  eff1i 8665  explogt 8694  reexplogt 8695  relogexpt 8696  logexptOLD 8712  explogtOLD 8713  hvmul0t 8814  hvmul0ort 8815  hvsubidt 8816  hvm1negt 8822  hvadd12t 8825  hvadd4t 8826  hvpncan2t 8830  hvmulcomt 8833  hvsubdistr2t 8838  hvsubsub4t 8848  hvaddsub4t 8866  his52t 8875  hiassdit 8878  his2subt 8879  normlem6 8902  normlem7tALT 8906  bcseq 8907  normlem9at 8908  normsqt 8922  norm-iit 8926  norm-iiit 8928  normpytht 8933  norm3dift 8938  norm3dif2t 8939  norm3adift 8941  normpart 8943  polidt 8947  hhph 8966  bcst 8969  hcau2 8976  hlim 8977  hlim2 8981  hlim0 9026  hlimcaui 9027  norm1t 9042  chocuni 9088  occllem2 9090  occllem3 9091  occllem5 9093  occllem6 9094  projlem7 9108  projlem22 9123  projlem23 9124  projlem25 9126  projlem26 9127  pjthlem7 9140  pjthlem8 9141  pjthlem9 9142  chdmm1t 9363  chdmm2t 9364  chjasst 9371  chj12t 9372  ledit 9378  spanunt 9383  h1de2b 9392  h1de2bOLD 9393  elspansn2t 9406  spansncol 9407  normcant 9416  pjspansnt 9417  spanunsn 9419  h1datom 9421  hosmvalt 9428  hodmvalt 9430  hfsmvalt 9431  cmbr3t 9468  pjoml3t 9472  fh2t 9479  osumlem2 9496  5oalem2 9517  3oalem2 9525  pjadjt 9547  pjaddt 9548  pjinormt 9549  pjsubt 9550  pjige0t 9553  pjcjt2 9554  pjds3 9575  pjopytht 9582  pjpytht 9587  mayete3 9590  hoaddass 9619  hoaddasst 9625  hoadd4t 9627  hocsubdirt 9628  homul12t 9648  hoaddsubt 9659  adjmo 9675  adjsymt 9676  eigpos 9679  eigortht 9681  elhmopt 9717  eigvalvalt 9740  lnoplt 9754  unopt 9755  hmopt 9762  lnfnlt 9771  adjt 9773  adjeqt 9775  hmopadj2t 9781  bralnfnt 9788  kbvalt 9792  kbvalvalt 9794  kbmult 9795  kbpjt 9796  eigvalt 9800  eigvect 9802  lnop0t 9806  lnopadd 9811  lnopmulsub 9816  0hmop 9823  hoddit 9830  adj0 9834  lnopeq0lem2 9846  lnopeq0 9847  lnopeq 9848  lnopeqt 9849  lnopuni 9852  lnophm 9858  hmopst 9860  hmopmt 9861  hmopcot 9863  nmbdoplb 9864  nmbdoplbt 9865  nmcopexlem3 9868  nmcopexlem5 9870  nmcoplb 9873  nmcoplbt 9875  nmophm 9876  lnfnadd 9887  nmbdfnlb 9893  nmbdfnlbt 9894  nmcfnexlem3 9897  nmcfnexlem5 9899  nmcfnlb 9902  nmcfnlbt 9904  nlelch 9909  cnlnadjlem1 9915  cnlnadjlem2 9916  cnlnadjlem5 9919  cnlnadjeut 9926  cnlnssadj 9928  adjmult 9939  adjaddt 9940  nmopco 9942  adjco 9947  unierr 9950  cnvbramult 9960  kbass1t 9961  kbass5t 9965  kbass6t 9966  leopg 9967  leop2t 9969  leop3t 9970  leoppost 9971  leoprf2t 9972  leoprft 9973  leopsqt 9974  idleop 9976  leopaddt 9977  leopmulit 9978  leopmult 9979  leopnmidt 9982  nmopleidt 9983  hmopidmchlem 9989  hmopidmch 9990  pjadjco 10000  pjsspos 10011  pjssdif2 10013  pjssdif1 10014  pjclem4 10037  pjadj2co 10042  pj3s 10045  pj3cor1 10047  hstel2t 10056  hstnmoct 10060  hst1ht 10064  hstpytht 10066  stjt 10072  strlem1 10087  strlem2 10088  strlem3a 10089  strlem4 10091  golem1 10108  mdbr3 10134  mdbr4 10135  dmdbrt 10136  dmdmdt 10137  dmdit 10139  dmdbr3 10141  dmdbr4 10142  dmdi4 10143  mdslmd1lem1 10160  mdslmd1lem3 10162  mdslmd1lem4 10163  sumdmdlem2 10253  cdj3lem1 10266  cdj3lem2b 10269  cdj3lem3b 10272  cdj3 10273  abs2sqlet 10279  abs2sqltt 10280  ghomgrpilem1 10290  ghomlin 10298  symggrpiOLD 10311  symggrpi 10313  cayleylem2 10317  hmeogrp 10425  mslb1 10473  2wsms 10474  iscat 10531  cati 10532  1cat 10536  cmpasso 10550  cmpida 10551  idmon 10588

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