Theorem opreq12d 3917

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

Syntax hints:   -> wi 3   = wceq 1099  (class class class)co 3902

This theorem is referenced by:  hboprd 3921  csboprg 3925  elimdeloprv 3940  caoprdistr 3999  oesuc 4104  odi 4148  nnmsucr 4178  ecoprdi 4259  ltaddpq 5002  halfpq 5005  prlem934a 5060  prlem936a 5076  adddirt 5242  muladdt 5344  muladd11t 5345  subdirt 5351  mulsubt 5400  pnpcan2t 5402  msqgt0t 5540  msqge0t 5541  recextlem1 5606  muleqaddt 5620  divcan1z 5638  divcan2z 5639  divcan1t 5640  divcan2t 5641  recidt 5649  divdirz 5663  divdirt 5664  divcan3z 5667  divcan3t 5669  divadddivt 5691  conjmult 5704  2timest 5902  seq1rval 6199  seq1suclem 6204  ser1add2 6226  ser1add 6227  icoshftf1olem 6294  fzrev3t 6397  fzrevral2t 6403  fzrevral3t 6404  fzshftralt 6405  seqzfval 6420  mulexpt 6476  expubndt 6490  subsqt 6524  binom2t 6532  discrlem2 6538  discrlem3 6539  discrlem 6540  nn0opth 6547  nn0opth2t 6549  sqrlem21 6574  sqrth 6580  absvalt 6645  cjvalt 6646  imret 6661  cjmulrclt 6687  cjmulvalt 6688  cjmulge0t 6689  addcjt 6701  recjt 6704  imcjt 6705  cjreimt 6714  cjreim2t 6715  sqabsaddt 6734  sqabssubt 6735  absval2t 6738  absreimsqt 6742  recant 6793  abslem2 6797  facp1t 6824  faclbnd4lem1 6836  faclbnd4lem2 6837  faclbnd4lem3 6838  faclbnd4lem4 6839  bcvalt 6846  bcn0t 6852  bcnp11t 6854  bcpasc2t 6857  bcpasc 6858  bcpasct 6859  fsump1 6895  fsump1slem 6901  fsump1s 6902  fsum1ps 6907  fsumsplit 6909  fsumadd 6911  fsum3 6913  fsum4 6914  fsumrev2 6919  fsumshft 6920  fsumshftm 6921  fsummulc1 6922  ser1ser0 6937  serzsplit 6945  binomlem1 6955  binomlem2 6956  binomlem3 6957  binomlem4 6958  binomlem5 6959  binomlem6 6960  binom 6961  climaddlem1 7001  climmullem5 7011  climmullem6 7012  climcmplem 7024  caucvg3a 7051  caucvg3lem 7053  caucvg3t 7055  fnsmnt 7112  geolim1 7125  georeclim 7126  fsum0diaglem2 7143  fsum0diag2 7145  elcncf 7151  mulc1cncf 7165  efcltlem1 7197  dfef2 7200  ef0lem 7203  efclt 7205  efcvg 7207  eftval 7209  erelem6 7217  efcj 7229  efaddlem6 7236  efaddlem24 7254  efaddlem26 7256  efaddlem27 7257  eftabs 7268  ef1tlub 7275  ef01tllem1 7276  ef01tllem2 7277  ef01tlub 7278  absef01tlub 7280  ef4pt 7292  absefm1le 7303  efm1legeot 7309  efcnlem4 7313  sinvalt 7322  cosvalt 7323  efi4pt 7328  sinnegt 7335  cosnegt 7336  efivalt 7340  efmivalt 7341  sinaddt 7346  cosaddt 7347  sinsubt 7348  cossubt 7349  addsint 7350  subsint 7351  addcost 7352  subcost 7353  sincossqt 7354  cos2tt 7356  cos01bndlem3 7364  demoivre 7377  xpnnen 7392  ruclem4 7407  ismet 7685  ismsg 7687  msflem 7690  mettri2 7700  mettri4 7701  cnmet 7791  ioo2bl 7799  dscmet 7804  iscau 7822  bopcnlem2 7864  fsumcnlem 7871  bcthlem15 7895  bcthlem16 7896  bcthlem17 7897  bcthlem18 7898  bcthlem21 7901  bcthlem24 7904  bcthlem28 7908  grpnnncan2 7976  isring 8026  ringi 8027  ringdi 8031  ringdir 8032  ringsn 8048  isvcg 8052  vci 8054  vcdi 8058  vcdir 8059  vc2 8061  isnvg 8109  nvi 8111  nvaddsub4 8158  imsmetlem 8198  ipval2 8226  ipval3 8228  ipid 8232  ipcj 8236  ip0r 8239  islno 8283  0lno 8317  isphg 8342  cnph 8344  phpar2 8348  phpar 8349  ipdiri 8355  ipasslem6 8361  ipasslem8 8363  ipasslem9 8364  ipdir 8368  ipdi 8369  ipsubdi 8375  pythi 8376  sspph 8381  ipblnfi 8382  minveclem33 8443  minveclem35 8445  sincolem 8497  sinper 8522  cosper 8523  sinmpi 8526  cosmpi 8527  efimpi 8528  sinhalfpip 8529  sinhalfpim 8530  coshalfpip 8531  coshalfpim 8532  shftefif1olem 8574  shftefif1olemOLD 8575  effoi 8579  effoiOLD 8580  efper 8582  elghomlem2 8650  iintlem1 8826  iintlem2 8827  1cat 8886  isfunb 8941  hvsub4t 9055  his7t 9105  his2sub2t 9108  normlem6 9130  normlem7tALT 9134  bcseq 9135  normlem9at 9136  normsqt 9150  normpyth 9158  norm3dift 9166  normpart 9171  polidt 9175  hcau 9201  pjthlem7 9354  pjthlem8 9355  axpjpjt 9385  chjot 9567  ledit 9592  elspansn2t 9620  normcant 9630  hosvalt 9647  hosvaltOLD 9648  hodvalt 9650  hodvaltOLD 9651  hfsvalt 9652  cmbrt 9658  pjoml2t 9685  cm2jt 9694  pjinormt 9763  pjcjt2 9768  pjopytht 9796  pjpytht 9801  mayete3 9804  hocadddir 9836  hocsubdir 9837  hocsubdirt 9842  hodidt 9849  hoadddit 9860  hoadddirt 9861  hosub4t 9870  eigret 9892  elcnopt 9914  ellnopt 9915  elunopt 9930  elcnfnt 9940  ellnfnt 9941  unopf1ot 9970  cnvunopt 9972  unoplint 9974  counopt 9975  hmoplint 9996  braaddt 9999  eigvalt 10014  hoddi 10043  hoddit 10044  lnophs 10055  lnopeq0lem2 10060  lnopeq0 10061  lnopunilem1 10064  lnophmlem1 10070  lnophmt 10073  riesz3 10124  riesz4 10125  cnlnadjlem6 10134  adjlnopt 10148  adjaddt 10154  unierr 10164  kbass2t 10176  pjsdi 10208  pjddi 10209  pjssmt 10218  pjssge0t 10219  pjdifnormt 10220  pjsspos 10225  pjclem1 10247  pjc 10252  stelt 10265  hstelt 10266  hstoht 10283  golem1 10322  mdslmd1lem1 10374  irredlem2 10440  irredlem3 10441

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-pow 2710  ax-pr 2747

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-xp 3147  df-cnv 3149  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fv 3161  df-opr 3904

Copyright terms: Public domain