Theorem opreq12i 4031

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 4029	. 2 |- (AFC) = (BFC)
3		opreq12i.2	. . 3 |- C = D
4	3	opreq2i 4030	. 2 |- (BFC) = (BFD)
5	2, 4	eqtri 1542	1 |- (AFC) = (BFD)

Syntax hints:   = wceq 997  (class class class)co 4021

This theorem is referenced by:  caoprdistrr 4125  caoprdilem 4126  caoprlem2 4127  addcmpblnq 5117  addcompq 5127  addasspq 5128  distrpq 5132  1lt2pq 5143  mulcomsr 5263  distrsr 5265  m1p1sr 5266  m1m1sr 5267  mulgt0sr 5279  addcnsrec 5328  mulcnsrec 5329  axmulcom 5341  axmulass 5343  axdistr 5344  axi2m1 5350  1p1timesi 5498  mulneg1i 5510  negdii 5513  divdiri 5810  3t3e9 6085  halfpm6th 6093  nneoi 6282  icoshftf1oii 6435  ser1add2i 6597  ser1addi 6598  seq1seqz 6630  seq0seqz 6631  seq01 6641  sqdivi 6707  sumsqne0i 6723  binom2i 6733  binom2aiOLD 6734  discrlem1 6746  nnesqi 6752  nn0opthlem1 6754  sqrlem11 6773  sqrlem16 6778  sqrthi 6789  sqrmulii 6794  i4 6824  crmuli 6830  crreczi 6831  cjcji 6868  readdi 6874  imaddi 6875  remuli 6876  immuli 6877  cjaddi 6878  cjmuli 6879  ipcni 6880  cjmulvali 6882  cjnegi 6887  addcji 6888  cji 6917  absmuli 6937  abs1mi 6994  abslem2i 6998  facp1 7026  fac2 7027  fac3 7028  faclbnd4lem1 7038  bcpasc2i 7057  isumnn0nnai 7298  0.999... 7336  dfef2i 7397  efaddlem5 7432  efaddlem6 7433  efaddlem12 7439  eirrlem3 7481  efsepi 7487  eft0vali 7489  ef4pi 7490  efge1pi 7493  efcnlem2 7511  sinaddi 7542  cosaddi 7543  cos2OLD 7556  sin01bndlem3 7561  cos2bnd 7567  ruclem15 7616  bcthlem32 8115  ipval2lem1 8435  ipval2 8441  ip0i 8568  ip1ilem 8569  ip2i 8571  ipdirilem 8572  ipasslem10 8583  ip2dii 8588  pythi 8594  siilem1 8595  eulerid 8766  sin2pi 8767  sinperlem1 8769  sincosq3sgn 8789  sincosq4sgn 8790  sincos4thpi 8793  sincos6thpi 8794  hvsubsub4i 9009  hvsubcan2i 9014  hisubcomi 9053  normlem0 9058  normlem1 9059  normlem2 9060  normlem3 9061  normlem6 9064  normlem8 9066  normlem9 9067  bcseqi 9069  norm-ii.i 9087  norm-iii.i 9089  normpythi 9092  norm3difi 9097  normpari 9104  normpar2i 9106  polid2i 9107  polidi 9108  bcsiALT 9129  projlem3 9271  projlem4 9272  pjthlem5 9306  lediri 9543  h1de2i 9559  cmcmlem 9617  cmbr2i 9622  cm2j 9646  fh3i 9649  fh4i 9650  pjaddii 9703  pjsslem 9707  pjssmii 9709  pjdifnormii 9711  hhlnoi 9909  lnopeq0lem1 10013  lnopunilem1 10018  lnophmlem2 10025  pjsdi2i 10168  pjclem1 10207  golem1 10282  1cat 10774

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