Theorem opreq12d 3973

Description: Equality deduction for operation value.

Hypotheses

Ref	Expression
opreq1d.1	⊢ (φ → A = B)
opreq12d.2	⊢ (φ → C = D)

Assertion

Ref	Expression
opreq12d	⊢ (φ → (AFC) = (BFD))

Proof of Theorem opreq12d

Step	Hyp	Ref	Expression
1		opreq1d.1	. . 3 ⊢ (φ → A = B)
2	1	opreq1d 3970	. 2 ⊢ (φ → (AFC) = (BFC))
3		opreq12d.2	. . 3 ⊢ (φ → C = D)
4	3	opreq2d 3971	. 2 ⊢ (φ → (BFC) = (BFD))
5	2, 4	eqtrd 1505	1 ⊢ (φ → (AFC) = (BFD))

Syntax hints:   → wi 3   = wceq 955  (class class class)co 3958

This theorem is referenced by:  hboprd 3977  csboprg 3981  elimdeloprv 3996  caoprdistr 4054  oesuc 4159  odi 4203  nnmsucr 4233  ecoprdi 4314  ltaddpq 5062  halfpq 5065  prlem934a 5120  prlem936a 5136  adddirt 5302  muladdt 5404  muladd11t 5405  subdirt 5411  mulsubt 5460  pnpcan2t 5462  msqgt0t 5599  msqge0t 5600  recextlem1 5665  muleqaddt 5679  divcan1z 5697  divcan2z 5698  divcan1t 5699  divcan2t 5700  recidt 5708  divdirz 5722  divdirt 5723  divcan3z 5726  divcan3t 5728  divadddivt 5750  conjmult 5763  2timest 5961  seq1rval 6261  seq1suclem 6266  ser1add2 6288  ser1add 6289  icoshftf1olem 6356  fzrev3t 6459  fzrevral2t 6465  fzrevral3t 6466  fzshftralt 6467  seqzfval 6482  mulexpt 6539  expubndt 6553  subsqt 6587  binom2t 6595  discrlem2 6602  discrlem3 6603  discrlem 6604  nn0opth 6611  nn0opth2t 6613  sqrlem21 6638  sqrth 6644  absvalt 6709  cjvalt 6710  imret 6725  cjmulrclt 6751  cjmulvalt 6752  cjmulge0t 6753  addcjt 6765  recjt 6768  imcjt 6769  cjreimt 6778  cjreim2t 6779  sqabsaddt 6798  sqabssubt 6799  absval2t 6802  absreimsqt 6806  recant 6857  abslem2 6861  facp1t 6888  faclbnd4lem1 6900  faclbnd4lem2 6901  faclbnd4lem3 6902  faclbnd4lem4 6903  bcvalt 6910  bcn0t 6916  bcnp11t 6918  bcpasc2t 6921  bcpasc 6922  bcpasct 6923  fsump1 6959  fsump1slem 6965  fsump1s 6966  fsum1ps 6971  fsumsplit 6973  fsumadd 6975  fsum3 6977  fsum4 6978  fsumrev2 6983  fsumshft 6984  fsumshftm 6985  fsummulc1 6986  ser1ser0 7001  serzsplit 7009  binomlem1 7019  binomlem2 7020  binomlem3 7021  binomlem4 7022  binomlem5 7023  binomlem6 7024  binom 7025  climaddlem1 7067  climmullem5 7077  climmullem6 7078  climcmplem 7090  caucvg3a 7117  caucvg3lem 7119  caucvg3t 7121  fnsmnt 7178  geolim1 7191  georeclim 7192  fsum0diaglem2 7209  fsum0diag2 7211  elcncf 7217  mulc1cncf 7231  efcltlem1 7263  dfef2 7266  ef0lem 7269  efclt 7271  efcvg 7273  eftval 7275  erelem6 7283  efcj 7295  efaddlem6 7302  efaddlem24 7320  efaddlem26 7322  efaddlem27 7323  eftabs 7334  ef1tlub 7341  ef01tllem1 7342  ef01tllem2 7343  ef01tlub 7344  absef01tlub 7346  ef4pt 7358  absefm1le 7369  efm1legeot 7375  efcnlem4 7379  sinvalt 7388  cosvalt 7389  efi4pt 7394  sinnegt 7401  cosnegt 7402  efivalt 7406  efmivalt 7407  sinaddt 7412  cosaddt 7413  sinsubt 7414  cossubt 7415  addsint 7416  subsint 7417  addcost 7418  subcost 7419  sincossqt 7420  cos2tt 7422  cos01bndlem3 7430  demoivre 7443  xpnnen 7458  ruclem4 7473  ismet 7758  ismsg 7760  msflem 7763  mettri2 7773  mettri4 7774  cnmet 7866  ioo2bl 7874  dscmet 7880  iscau 7898  bopcnlem2 7944  fsumcnlem 7951  bcthlem15 7975  bcthlem16 7976  bcthlem17 7977  bcthlem18 7978  bcthlem21 7981  bcthlem24 7984  bcthlem28 7988  grpnnncan2 8055  isring 8105  ringi 8106  ringdi 8110  ringdir 8111  ringsn 8127  vci 8131  vcdi 8135  vcdir 8136  vc2 8138  isvclem 8160  isnvlem 8193  nvi 8197  nvaddsub4 8245  imsmetlem 8287  ipval2 8319  ipval3 8321  ipid 8325  ipcj 8329  ip0r 8332  islno 8376  0lno 8410  isphg 8435  cnph 8437  phpar2 8441  phpar 8442  ipdiri 8448  ipasslem6 8454  ipasslem8 8456  ipasslem9 8457  ipdir 8461  ipdi 8462  ipsubdi 8468  pythi 8469  sspph 8474  ipblnfi 8475  minveclem33 8536  minveclem35 8538  sincolem 8619  sinper 8644  cosper 8645  sinmpi 8648  cosmpi 8649  efimpi 8650  sinhalfpip 8651  sinhalfpim 8652  coshalfpip 8653  coshalfpim 8654  shftefif1olem 8696  effoi 8700  efper 8702  hvsub4t 8861  his7t 8911  his2sub2t 8914  normlem6 8936  normlem7tALT 8940  bcseq 8941  normlem9at 8942  normsqt 8956  normpyth 8964  norm3dift 8972  normpart 8977  polidt 8981  hcau 9006  hhssnv 9089  pjthlem7 9180  pjthlem8 9181  axpjpjt 9211  chjot 9393  ledit 9418  elspansn2t 9446  normcant 9456  hosvalt 9473  hosvaltOLD 9474  hodvalt 9476  hodvaltOLD 9477  hfsvalt 9478  cmbrt 9484  pjoml2t 9511  cm2jt 9520  pjinormt 9589  pjcjt2 9594  pjopytht 9622  pjpytht 9627  mayete3 9630  hocadddir 9662  hocsubdir 9663  hocsubdirt 9668  hodidt 9675  hoadddit 9686  hoadddirt 9687  hosub4t 9696  eigret 9718  elcnopt 9740  ellnopt 9741  elunopt 9756  elcnfnt 9766  ellnfnt 9767  unopf1ot 9797  cnvunopt 9799  unoplint 9801  counopt 9802  hmoplint 9823  braaddt 9826  eigvalt 9841  hoddi 9870  hoddit 9871  lnophs 9882  lnopeq0lem2 9887  lnopeq0 9888  lnopunilem1 9891  lnophmlem1 9897  lnophmt 9900  riesz3 9951  riesz4 9952  cnlnadjlem6 9961  adjlnopt 9975  adjaddt 9982  unierr 9993  kbass2t 10006  pjsdi 10039  pjddi 10040  pjssmt 10049  pjssge0t 10050  pjdifnormt 10051  pjsspos 10056  pjclem1 10079  pjc 10084  stelt 10097  hstelt 10098  hstoht 10115  golem1 10154  mdslmd1lem1 10208  irredlem2 10274  irredlem3 10275  elghomlem2 10339  iintlem1 10548  iintlem2 10549  1cat 10608  isfunb 10665

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-sep 2699  ax-pow 2738  ax-pr 2775

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409  df-pr 2410  df-op 2413  df-uni 2500  df-br 2616  df-opab 2663  df-xp 3180  df-cnv 3182  df-dm 3184  df-rn 3185  df-res 3186  df-ima 3187  df-fv 3194  df-opr 3960

Copyright terms: Public domain