Theorem opreq12i 3970

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 3968	. 2 |- (AFC) = (BFC)
3		opreq12i.2	. . 3 |- C = D
4	3	opreq2i 3969	. 2 |- (BFC) = (BFD)
5	2, 4	eqtr 1494	1 |- (AFC) = (BFD)

Syntax hints:   = wceq 955  (class class class)co 3960

This theorem is referenced by:  caoprdistrr 4064  caoprdilem 4065  caoprlem2 4066  addcmpblnq 5039  addcompq 5049  addasspq 5050  distrpq 5054  1lt2pq 5065  mulcomsr 5185  distrsr 5187  m1p1sr 5188  m1m1sr 5189  mulgt0sr 5201  addcnsrec 5250  mulcnsrec 5251  axmulcom 5263  axmulass 5265  axdistr 5266  axi2m1 5272  1p1times 5420  mulneg1 5432  negdi 5435  divdir 5724  3t3e9 5985  halfpm6th 5993  nneo 6158  ser1add2 6293  ser1add 6294  icoshftf1oi 6360  seq1seqz 6491  seq0seqz 6492  seq01 6502  sqdiv 6568  sumsqne0 6584  binom2 6594  binom2aOLD 6595  discrlem1 6606  nnesq 6612  nn0opthlem1 6614  sqrlem11 6634  sqrlem16 6639  sqrth 6650  sqrmuli 6655  i4 6685  crmul 6692  crrecz 6693  cjcj 6736  readd 6743  imadd 6744  remul 6745  immul 6746  cjadd 6747  cjmul 6748  ipcn 6749  cjmulval 6751  cjneg 6758  addcj 6759  cji 6788  absmul 6809  abs1m 6869  abslem2i 6874  facp1t 6902  fac2 6903  fac3 6904  faclbnd4lem1 6914  bcpasc2 6935  isumnn0nna 7179  0.999... 7217  dfef2 7285  efaddlem5 7320  efaddlem6 7321  efaddlem12 7327  eirrlem3 7368  efsep 7373  eft0val 7375  ef4p 7376  efge1p 7379  efcnlem2 7396  sinadd 7429  cosadd 7430  cos2tOLD 7442  sin01bndlem3 7447  cos2bnd 7453  ruclem15 7503  bcthlem32 8013  ipval2lem1 8337  ipval2 8343  ip0i 8468  ip1ilem 8469  ip2i 8471  ipdirilem 8472  ipasslem10 8483  ip2dii 8488  pythi 8494  siilem1 8495  eulerid 8666  sin2pi 8667  sinperlem1 8669  sincosq3sgn 8687  sincosq4sgn 8688  sincos4thpi 8691  sincos6thpi 8692  hvsubsub4 8910  hvsubcan2 8915  hisubcom 8954  normlem0 8959  normlem1 8960  normlem2 8961  normlem3 8962  normlem6 8965  normlem8 8967  normlem9 8968  bcseq 8970  norm-ii 8988  norm-iii 8990  normpyth 8993  norm3dif 8998  normpar 9005  normpar2 9007  polid2 9008  polid 9009  bcsALT 9034  projlem3 9176  projlem4 9177  pjthlem5 9211  ledir 9448  h1de2 9464  cmcmlem 9524  cmbr2 9529  cm2jt 9553  fh3 9556  fh4 9557  pjadd 9611  pjsslem 9615  pjssm 9617  pjdifnorm 9619  hhlno 9817  lnopeq0lem1 9921  lnopunilem1 9926  lnophmlem2 9933  pjsdi2 10076  pjclem1 10114  golem1 10189  1cat 10643

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2700  ax-pow 2739  ax-pr 2776

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-v 1810  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-nul 2279  df-pw 2400  df-sn 2410  df-pr 2411  df-op 2414  df-uni 2501  df-br 2617  df-opab 2664  df-xp 3181  df-cnv 3183  df-dm 3185  df-rn 3186  df-res 3187  df-ima 3188  df-fv 3195  df-opr 3962

Copyright terms: Public domain