Theorem opreq12i 3979

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 3977	. 2 ⊢ (AFC) = (BFC)
3		opreq12i.2	. . 3 ⊢ C = D
4	3	opreq2i 3978	. 2 ⊢ (BFC) = (BFD)
5	2, 4	eqtr 1498	1 ⊢ (AFC) = (BFD)

Syntax hints:   = wceq 958  (class class class)co 3969

This theorem is referenced by:  caoprdistrr 4073  caoprdilem 4074  caoprlem2 4075  addcmpblnq 5064  addcompq 5074  addasspq 5075  distrpq 5079  1lt2pq 5090  mulcomsr 5210  distrsr 5212  m1p1sr 5213  m1m1sr 5214  mulgt0sr 5226  addcnsrec 5275  mulcnsrec 5276  axmulcom 5288  axmulass 5290  axdistr 5291  axi2m1 5297  1p1times 5445  mulneg1 5457  negdi 5460  divdir 5754  3t3e9 6026  halfpm6th 6034  nneo 6199  ser1add2 6339  ser1add 6340  icoshftf1oi 6410  seq1seqz 6542  seq0seqz 6543  seq01 6553  sqdiv 6619  sumsqne0 6635  binom2 6645  binom2aOLD 6646  discrlem1 6657  nnesq 6663  nn0opthlem1 6665  sqrlem11 6684  sqrlem16 6689  sqrth 6700  sqrmuli 6705  i4 6735  crmul 6741  crrecz 6742  cjcj 6778  readd 6784  imadd 6785  remul 6786  immul 6787  cjadd 6788  cjmul 6789  ipcn 6790  cjmulval 6792  cjneg 6797  addcj 6798  cji 6827  absmul 6847  abs1m 6904  abslem2i 6908  facp1t 6936  fac2 6937  fac3 6938  faclbnd4lem1 6948  bcpasc2 6967  isumnn0nna 7208  0.999... 7246  dfef2 7307  efaddlem5 7342  efaddlem6 7343  efaddlem12 7349  eirrlem3 7391  efsep 7396  eft0val 7398  ef4p 7399  efge1p 7402  efcnlem2 7420  sinadd 7451  cosadd 7452  cos2tOLD 7465  sin01bndlem3 7470  cos2bnd 7476  ruclem15 7525  bcthlem32 8027  ipval2lem1 8347  ipval2 8353  ip0i 8480  ip1ilem 8481  ip2i 8483  ipdirilem 8484  ipasslem10 8495  ip2dii 8500  pythi 8506  siilem1 8507  eulerid 8678  sin2pi 8679  sinperlem1 8681  sincosq3sgn 8701  sincosq4sgn 8702  sincos4thpi 8705  sincos6thpi 8706  hvsubsub4 8921  hvsubcan2 8926  hisubcom 8965  normlem0 8970  normlem1 8971  normlem2 8972  normlem3 8973  normlem6 8976  normlem8 8978  normlem9 8979  bcseq 8981  norm-ii 8999  norm-iii 9001  normpyth 9004  norm3dif 9009  normpar 9016  normpar2 9018  polid2 9019  polid 9020  bcsALT 9041  projlem3 9183  projlem4 9184  pjthlem5 9218  ledir 9455  h1de2 9471  cmcmlem 9529  cmbr2 9534  cm2jt 9558  fh3 9561  fh4 9562  pjadd 9615  pjsslem 9619  pjssm 9621  pjdifnorm 9623  hhlno 9821  lnopeq0lem1 9925  lnopunilem1 9930  lnophmlem2 9937  pjsdi2 10080  pjclem1 10118  golem1 10193  1cat 10663

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748  ax-pr 2785

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-xp 3190  df-cnv 3192  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fv 3204  df-opr 3971

Copyright terms: Public domain