Theorem opreq12d 4036

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 4033	. 2 |- (ph -> (AFC) = (BFC))
3		opreq12d.2	. . 3 |- (ph -> C = D)
4	3	opreq2d 4034	. 2 |- (ph -> (BFC) = (BFD))
5	2, 4	eqtrd 1554	1 |- (ph -> (AFC) = (BFD))

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

This theorem is referenced by:  hboprd 4040  csboprg 4044  elimdeloprv 4059  caoprdistr 4117  oesuc 4224  odi 4268  nnmsucr 4298  ecoprdi 4382  ltaddpq 5144  halfpq 5147  prlem934a 5202  prlem936a 5218  adddir 5384  muladd 5486  muladd11 5487  subdir 5493  mulsub 5542  pnpcan2 5544  msqgt0 5680  msqge0 5681  recextlem1 5747  muleqadd 5765  divcan1zi 5786  divcan2zi 5787  divcan1 5788  recid 5797  divdirzi 5812  divdir 5813  divdirOLD 5814  divcan3zi 5817  divcan3 5819  divadddiv 5842  conjmul 5855  2times 6065  modval 6372  icoshftf1olem 6436  fzrev3 6540  fzrevral2 6546  fzrevral3 6547  fzshftral 6548  seq1rval 6570  seq1suclem 6575  ser1add2i 6597  ser1addi 6598  seqzfval 6626  mulexp 6683  expubnd 6697  subsq 6731  binom2 6739  discrlem2 6747  discrlem3 6748  discrlem 6749  nn0opthi 6756  nn0opth2 6758  sqrlem21 6783  sqrthi 6789  absval 6852  cjval 6853  imre 6863  cjmulrcl 6891  cjmulval 6892  cjmulge0 6893  addcj 6905  recj 6908  imcj 6909  cjreim 6918  cjreim2 6919  sqabsadd 6938  sqabssub 6939  absval2 6942  absreimsq 6946  recan 6995  abslem2 6999  facp1 7026  faclbnd4lem1 7038  faclbnd4lem2 7039  faclbnd4lem3 7040  faclbnd4lem4 7041  bcval 7048  bcn0 7053  bcnp11 7055  bcpasc2 7058  bcpasci 7059  bcpasc 7060  fsump1i 7096  fsump1slem 7102  fsump1s 7103  fsum1ps 7108  fsumspl 7110  fsumadd 7112  fsum3 7114  fsum4 7115  fsumrev2 7120  fsumshf 7121  fsumshftm 7122  fsummulc1 7123  ser1ser0i 7138  serzsplit 7146  binomlem1 7156  binomlem2 7157  binomlem3 7158  binomlem4 7159  binomlem5 7160  binomlem6 7161  binomi 7162  climaddlem1 7204  climmullem5 7214  climmullem6 7215  climcmplem 7227  caucvg3ai 7254  caucvg3lem 7256  caucvg3 7258  arisumi 7316  geolim1 7329  georeclim 7330  fsum0diaglem2 7347  fsum0diag2 7349  elcncf 7355  mulc1cncf 7369  efcltlem1 7394  dfef2i 7397  ef0lem 7400  efcl 7402  efcvg 7404  eftval 7406  erelem6 7414  efcji 7426  efaddlem6 7433  efaddlem24 7451  efaddlem26 7453  efaddlem27 7454  eftabsi 7465  ef1tlubi 7472  ef01tllem1 7473  ef01tllem2 7474  ef01tllem2OLD 7475  ef01tlubi 7476  absef01tlubi 7478  ef4p 7491  absefm1lei 7503  efm1legeo 7509  efcnlem4 7513  sinval 7520  cosval 7521  efi4p 7526  sinneg 7533  cosneg 7534  efival 7538  efmival 7539  sinadd 7544  cosadd 7545  sinsub 7546  cossub 7547  addsin 7548  subsin 7549  addcos 7550  subcos 7551  sincossq 7552  cos2t 7554  cos01bndlem3 7563  demoivre 7576  xpnnen 7591  ruclem4 7605  ismet 7883  ismsg 7885  msflem 7888  mettri2 7898  mettri4 7899  cnmet 7989  ioo2bl 7997  dscmet 8003  iscau 8021  bopcnlem2 8067  fsumcnlem 8074  bcthlem15 8098  bcthlem16 8099  bcthlem17 8100  bcthlem18 8101  bcthlem21 8104  bcthlem24 8107  bcthlem28 8111  grpnnncan2 8177  isring 8225  ringi 8226  ringdi 8230  ringdir 8231  ringsn 8247  vci 8251  vcdi 8255  vcdir 8256  vc2 8258  isvclem 8280  isnvlem 8313  nvi 8317  nvaddsub4 8365  imsmetlem 8407  ipval2 8441  ipval3 8443  ipid 8447  ipcj 8451  ip0r 8454  islno 8498  0lno 8534  isphg 8560  cnph 8562  phpar2 8566  phpar 8567  ipdiri 8573  ipasslem6 8579  ipasslem8 8581  ipasslem9 8582  ipdir 8586  ipdi 8587  ipsubdi 8593  pythi 8594  sspph 8599  ipblnfi 8600  minveclem33 8661  minveclem35 8663  sincolem 8748  sinper 8773  cosper 8774  sinmpi 8777  cosmpi 8778  sinppi 8779  efimpi 8781  sinhalfpip 8782  sinhalfpim 8783  coshalfpip 8784  coshalfpim 8785  shftefif1olem 8824  effoi 8828  efper 8830  hvsub4 8989  his7 9039  his2sub2 9042  normlem6 9064  normlem7tALT 9068  bcseqi 9069  normlem9at 9070  normsq 9084  normpythi 9092  norm3dif 9100  normpar 9105  polid 9109  hcau 9134  hhssnv 9217  pjthlem7 9308  pjthlem8 9309  axpjpj 9339  chjo 9521  ledi 9546  elspansn2 9573  normcan 9582  hosval 9599  hosvalOLD 9600  hodval 9602  hodvalOLD 9603  hfsval 9604  cmbr 9610  pjoml2 9637  cm2j 9646  pjinormi 9715  pjcjt2 9720  pjopyth 9748  pjpyth 9753  mayete3i 9756  hocadddiri 9788  hocsubdiri 9789  hocsubdir 9794  hodid 9801  hoadddi 9812  hoadddir 9813  hosub4 9822  eigre 9844  elcnop 9866  ellnop 9867  elunop 9882  elcnfn 9892  ellnfn 9893  unopf1o 9923  cnvunop 9925  unoplin 9927  counop 9928  hmoplin 9949  braadd 9952  eigval1 9967  hoddii 9997  hoddi 9998  lnophsi 10009  lnopeq0lem2 10014  lnopeq0i 10015  lnopunilem1 10018  lnophmlem1 10024  lnophm 10027  riesz3i 10078  riesz4i 10079  cnlnadjlem6 10088  adjlnop 10102  adjadd 10109  unierri 10120  kbass2 10133  pjsdii 10166  pjddii 10167  pjssmi 10176  pjssge0i 10177  pjdifnormi 10178  pjssposi 10183  pjclem1 10207  pjci 10212  stel 10225  hstel 10226  hstoh 10243  golem1 10282  mdslmd1lem1 10336  irredlem2 10402  irredlem3 10403  elghomlem2 10468  vri 10583  iintlem1 10714  iintlem2 10715  1cat 10774  isfunb 10839

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