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 1538	1 |- (AFC) = (BFD)

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

This theorem is referenced by:  caoprdistrr 4128  caoprdilem 4129  caoprlem2 4130  addcmpblnq 5206  addcompq 5216  addasspq 5217  distrpq 5221  1lt2pq 5232  mulcomsr 5352  distrsr 5354  m1p1sr 5355  m1m1sr 5356  mulgt0sr 5368  addcnsrec 5417  mulcnsrec 5418  axmulcom 5430  axmulass 5432  axdistr 5433  axi2m1 5439  1p1timesi 5587  mulneg1i 5599  negdii 5602  divdiri 5893  3t3e9 6170  halfpm6th 6178  nneoi 6368  icoshftf1oii 6536  ser1add2i 6703  ser1addi 6704  seq1seqz 6736  seq0seqz 6737  seq01 6747  sqdivi 6815  sumsqne0i 6831  binom2i 6841  binom2aiOLD 6842  discrlem1 6857  nnesqi 6863  nn0opthlem1 6865  sqrlem11 6884  sqrlem16 6889  sqrthi 6900  sqrmulii 6905  i4 6935  crmuli 6941  crreczi 6942  cjcji 6979  readdi 6985  imaddi 6986  remuli 6987  immuli 6988  cjaddi 6989  cjmuli 6990  ipcni 6991  cjmulvali 6993  cjnegi 6998  addcji 6999  cji 7028  absmuli 7049  abs1mi 7107  abslem2i 7111  facp1 7139  fac2 7140  fac3 7141  faclbnd4lem1 7151  bcpasc2i 7170  isumnn0nnai 7412  0.999... 7451  dfef2i 7512  efaddlem5 7547  efaddlem6 7548  efaddlem12 7554  eirrlem3 7596  efsepi 7604  eft0vali 7606  ef4pi 7607  efge1pi 7610  efcnlem2 7628  sinaddi 7659  cosaddi 7660  cos2OLD 7673  sin01bndlem3 7678  cos2bnd 7684  ruclem15 7736  bcthlem32 8241  ipval2lem1 8605  ipval2 8611  ip0i 8740  ip1ilem 8741  ip2i 8743  ipdirilem 8744  ipasslem10 8755  ip2dii 8760  pythi 8766  siilem1 8767  eulerid 8950  sin2pi 8951  sinperlem1 8953  sincosq3sgn 8973  sincosq4sgn 8974  sinq34lt0t 8976  sincos4thpi 8978  sincos6thpi 8979  hvsubsub4i 9201  hvsubcan2i 9206  hisubcomi 9246  normlem0 9251  normlem1 9252  normlem2 9253  normlem3 9254  normlem6 9257  normlem8 9259  normlem9 9260  bcseqi 9262  norm-ii.i 9280  norm-iii.i 9282  normpythi 9285  norm3difi 9290  normpari 9297  normpar2i 9299  polid2i 9300  polidi 9301  bcsiALT 9322  projlem3 9464  projlem4 9465  pjthlem5 9499  lediri 9736  h1de2i 9752  cmcmlem 9810  cmbr2i 9815  cm2j 9839  fh3i 9842  fh4i 9843  pjaddii 9898  pjsslem 9902  pjssmii 9904  pjdifnormii 9906  hhlnoi 10106  lnopeq0lem1 10209  lnopunilem1 10214  lnophmlem2 10221  pjsdi2i 10365  pjclem1 10404  golem1 10479  1cat 11213  trirni 11896  bfplem6 12059  phtpycolem3 12095  phtpycolem4 12096

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-xp 3265  df-cnv 3267  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fv 3279  df-opr 4023

Copyright terms: Public domain