Theorem opreq12i 3964

Description: Equality inference for operation value.

Hypotheses

Ref	Expression
opreq1i.1	|- A = B
opreq12i.2	|- C = D

Assertion

Ref	Expression
opreq12i	|- (AFC) = (BFD)

Proof of Theorem opreq12i

Step	Hyp	Ref	Expression
1		opreq1i.1	. . 3 |- A = B
2	1	opreq1i 3962	. 2 |- (AFC) = (BFC)
3		opreq12i.2	. . 3 |- C = D
4	3	opreq2i 3963	. 2 |- (BFC) = (BFD)
5	2, 4	eqtr 1492	1 |- (AFC) = (BFD)

Syntax hints:   = wceq 954  (class class class)co 3954

This theorem is referenced by:  caoprdistrr 4059  caoprdilem 4060  caoprlem2 4061  addcmpblnq 5032  addcompq 5042  addasspq 5043  distrpq 5047  1lt2pq 5058  mulcomsr 5178  distrsr 5180  m1p1sr 5181  m1m1sr 5182  mulgt0sr 5194  addcnsrec 5243  mulcnsrec 5244  axmulcom 5256  axmulass 5258  axdistr 5259  axi2m1 5265  1p1times 5413  mulneg1 5425  negdi 5428  divdir 5718  3t3e9 5979  halfpm6th 5987  nneo 6152  ser1add2 6283  ser1add 6284  icoshftf1oi 6350  seq1seqz 6481  seq0seqz 6482  seq01 6492  sqdiv 6556  sumsqne0 6573  binom2 6583  binom2aOLD 6584  discrlem1 6594  nnesq 6600  nn0opthlem1 6602  sqrlem11 6621  sqrlem16 6626  sqrth 6637  sqrmuli 6642  i4 6672  crmul 6679  crrecz 6680  cjcj 6721  readd 6727  imadd 6728  remul 6729  immul 6730  cjadd 6731  cjmul 6732  ipcn 6733  cjmulval 6735  cjneg 6740  addcj 6741  cji 6770  absmul 6790  abs1m 6849  abslem2i 6853  facp1t 6881  fac2 6882  fac3 6883  faclbnd4lem1 6893  bcpasc2 6913  isumnn0nna 7151  0.999... 7189  dfef2 7257  efaddlem5 7292  efaddlem6 7293  efaddlem12 7299  eirrlem3 7340  efsep 7345  eft0val 7347  ef4p 7348  efge1p 7351  efcnlem2 7368  sinadd 7401  cosadd 7402  cos2tOLD 7414  sin01bndlem3 7419  cos2bnd 7425  ruclem15 7475  bcthlem32 7980  ipval2lem1 8298  ipval2 8304  ip0i 8428  ip1ilem 8429  ip2i 8431  ipdirilem 8432  ipasslem10 8443  ip2dii 8448  pythi 8454  siilem1 8455  eulerid 8621  sin2pi 8622  sinperlem1 8624  sincosq3sgn 8642  sincosq4sgn 8643  sincos4thpi 8646  sincos6thpi 8647  hvsubsub4 8865  hvsubcan2 8870  hisubcom 8909  normlem0 8914  normlem1 8915  normlem2 8916  normlem3 8917  normlem6 8920  normlem8 8922  normlem9 8923  bcseq 8925  norm-ii 8943  norm-iii 8945  normpyth 8948  norm3dif 8953  normpar 8960  normpar2 8962  polid2 8963  polid 8964  bcsALT 8985  projlem3 9127  projlem4 9128  pjthlem5 9161  ledir 9398  h1de2 9414  cmcmlem 9474  cmbr2 9479  cm2jt 9503  fh3 9506  fh4 9507  pjadd 9560  pjsslem 9564  pjssm 9566  pjdifnorm 9568  hhlno 9766  lnopeq0lem1 9868  lnopunilem1 9873  lnophmlem2 9880  pjsdi2 10023  pjclem1 10061  golem1 10136  1cat 10572

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-xp 3179  df-cnv 3181  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fv 3193  df-opr 3956

Copyright terms: Public domain