Theorem opreq12d 3963

Description: Equality deduction for operation value.

Hypotheses

Ref	Expression
opreq1d.1	|- (ph -> A = B)
opreq12d.2	|- (ph -> C = D)

Assertion

Ref	Expression
opreq12d	|- (ph -> (AFC) = (BFD))

Proof of Theorem opreq12d

Step	Hyp	Ref	Expression
1		opreq1d.1	. . 3 |- (ph -> A = B)
2	1	opreq1d 3960	. 2 |- (ph -> (AFC) = (BFC))
3		opreq12d.2	. . 3 |- (ph -> C = D)
4	3	opreq2d 3961	. 2 |- (ph -> (BFC) = (BFD))
5	2, 4	eqtrd 1499	1 |- (ph -> (AFC) = (BFD))

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

This theorem is referenced by:  hboprd 3967  csboprg 3971  elimdeloprv 3986  caoprdistr 4045  oesuc 4150  odi 4194  nnmsucr 4224  ecoprdi 4305  ltaddpq 5051  halfpq 5054  prlem934a 5109  prlem936a 5125  adddirt 5291  muladdt 5393  muladd11t 5394  subdirt 5400  mulsubt 5449  pnpcan2t 5451  msqgt0t 5589  msqge0t 5590  recextlem1 5655  muleqaddt 5669  divcan1z 5687  divcan2z 5688  divcan1t 5689  divcan2t 5690  recidt 5698  divdirz 5712  divdirt 5713  divcan3z 5716  divcan3t 5718  divadddivt 5740  conjmult 5753  2timest 5951  seq1rval 6248  seq1suclem 6253  ser1add2 6275  ser1add 6276  icoshftf1olem 6343  fzrev3t 6446  fzrevral2t 6452  fzrevral3t 6453  fzshftralt 6454  seqzfval 6469  mulexpt 6525  expubndt 6539  subsqt 6573  binom2t 6581  discrlem2 6587  discrlem3 6588  discrlem 6589  nn0opth 6596  nn0opth2t 6598  sqrlem21 6623  sqrth 6629  absvalt 6694  cjvalt 6695  imret 6710  cjmulrclt 6736  cjmulvalt 6737  cjmulge0t 6738  addcjt 6750  recjt 6753  imcjt 6754  cjreimt 6763  cjreim2t 6764  sqabsaddt 6783  sqabssubt 6784  absval2t 6787  absreimsqt 6791  recant 6842  abslem2 6846  facp1t 6873  faclbnd4lem1 6885  faclbnd4lem2 6886  faclbnd4lem3 6887  faclbnd4lem4 6888  bcvalt 6895  bcn0t 6901  bcnp11t 6903  bcpasc2t 6906  bcpasc 6907  bcpasct 6908  fsump1 6944  fsump1slem 6950  fsump1s 6951  fsum1ps 6956  fsumsplit 6958  fsumadd 6960  fsum3 6962  fsum4 6963  fsumrev2 6968  fsumshft 6969  fsumshftm 6970  fsummulc1 6971  ser1ser0 6986  serzsplit 6994  binomlem1 7004  binomlem2 7005  binomlem3 7006  binomlem4 7007  binomlem5 7008  binomlem6 7009  binom 7010  climaddlem1 7050  climmullem5 7060  climmullem6 7061  climcmplem 7073  caucvg3a 7100  caucvg3lem 7102  caucvg3t 7104  fnsmnt 7161  geolim1 7174  georeclim 7175  fsum0diaglem2 7192  fsum0diag2 7194  elcncf 7200  mulc1cncf 7214  efcltlem1 7246  dfef2 7249  ef0lem 7252  efclt 7254  efcvg 7256  eftval 7258  erelem6 7266  efcj 7278  efaddlem6 7285  efaddlem24 7303  efaddlem26 7305  efaddlem27 7306  eftabs 7317  ef1tlub 7324  ef01tllem1 7325  ef01tllem2 7326  ef01tlub 7327  absef01tlub 7329  ef4pt 7341  absefm1le 7352  efm1legeot 7358  efcnlem4 7362  sinvalt 7371  cosvalt 7372  efi4pt 7377  sinnegt 7384  cosnegt 7385  efivalt 7389  efmivalt 7390  sinaddt 7395  cosaddt 7396  sinsubt 7397  cossubt 7398  addsint 7399  subsint 7400  addcost 7401  subcost 7402  sincossqt 7403  cos2tt 7405  cos01bndlem3 7413  demoivre 7426  xpnnen 7441  ruclem4 7456  ismet 7737  ismsg 7739  msflem 7742  mettri2 7752  mettri4 7753  cnmet 7843  ioo2bl 7851  dscmet 7856  iscau 7874  bopcnlem2 7916  fsumcnlem 7923  bcthlem15 7947  bcthlem16 7948  bcthlem17 7949  bcthlem18 7950  bcthlem21 7953  bcthlem24 7956  bcthlem28 7960  grpnnncan2 8028  isring 8078  ringi 8079  ringdi 8083  ringdir 8084  ringsn 8100  vci 8104  vcdi 8108  vcdir 8109  vc2 8111  isvcgOLD 8133  isvclem 8134  isnvlem 8167  isnvgOLD 8168  nvi 8173  nvaddsub4 8221  imsmetlem 8261  ipval2 8291  ipval3 8293  ipid 8297  ipcj 8301  ip0r 8304  islno 8348  0lno 8382  isphg 8407  cnph 8409  phpar2 8413  phpar 8414  ipdiri 8420  ipasslem6 8426  ipasslem8 8428  ipasslem9 8429  ipdir 8433  ipdi 8434  ipsubdi 8440  pythi 8441  sspph 8446  ipblnfi 8447  minveclem33 8508  minveclem35 8510  sincolem 8584  sinper 8609  cosper 8610  sinmpi 8613  cosmpi 8614  efimpi 8615  sinhalfpip 8616  sinhalfpim 8617  coshalfpip 8618  coshalfpim 8619  shftefif1olem 8661  shftefif1olemOLD 8662  effoi 8666  effoiOLD 8667  efper 8669  hvsub4t 8827  his7t 8877  his2sub2t 8880  normlem6 8902  normlem7tALT 8906  bcseq 8907  normlem9at 8908  normsqt 8922  normpyth 8930  norm3dift 8938  normpart 8943  polidt 8947  hcau 8972  hhssnv 9054  pjthlem7 9140  pjthlem8 9141  axpjpjt 9171  chjot 9353  ledit 9378  elspansn2t 9406  normcant 9416  hosvalt 9433  hosvaltOLD 9434  hodvalt 9436  hodvaltOLD 9437  hfsvalt 9438  cmbrt 9444  pjoml2t 9471  cm2jt 9480  pjinormt 9549  pjcjt2 9554  pjopytht 9582  pjpytht 9587  mayete3 9590  hocadddir 9622  hocsubdir 9623  hocsubdirt 9628  hodidt 9635  hoadddit 9646  hoadddirt 9647  hosub4t 9656  eigret 9678  elcnopt 9700  ellnopt 9701  elunopt 9716  elcnfnt 9726  ellnfnt 9727  unopf1ot 9756  cnvunopt 9758  unoplint 9760  counopt 9761  hmoplint 9782  braaddt 9785  eigvalt 9800  hoddi 9829  hoddit 9830  lnophs 9841  lnopeq0lem2 9846  lnopeq0 9847  lnopunilem1 9850  lnophmlem1 9856  lnophmt 9859  riesz3 9910  riesz4 9911  cnlnadjlem6 9920  adjlnopt 9934  adjaddt 9940  unierr 9950  kbass2t 9962  pjsdi 9994  pjddi 9995  pjssmt 10004  pjssge0t 10005  pjdifnormt 10006  pjsspos 10011  pjclem1 10033  pjc 10038  stelt 10051  hstelt 10052  hstoht 10069  golem1 10108  mdslmd1lem1 10160  irredlem2 10226  irredlem3 10227  elghomlem2 10288  iintlem1 10476  iintlem2 10477  1cat 10536  isfunb 10593

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