Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem opreq12i 3958

Description: Equality inference for operation value.

Hypotheses

Ref	Expression
opreq1i.1
opreq12i.2

Assertion

Ref	Expression
opreq12i

---

Proof of Theorem opreq12i

Step	Hyp	Ref	Expression
1		opreq1i.1	. . 3
2	1	opreq1i 3956	. 2
3		opreq12i.2	. . 3
4	3	opreq2i 3957	. 2
5	2, 4	eqtr 1487	1

Colors of variables: wff set class

Syntax hints:   wceq 953  (class class class)co 3948

This theorem is referenced by:  caoprdistrr 4053  caoprdilem 4054  caoprlem2 4055  addcmpblnq 5024  addcompq 5034  addasspq 5035  distrpq 5039  1lt2pq 5050  mulcomsr 5170  distrsr 5172  m1p1sr 5173  m1m1sr 5174  mulgt0sr 5186  addcnsrec 5235  mulcnsrec 5236  axmulcom 5248  axmulass 5250  axdistr 5251  axi2m1 5257  1p1times 5405  mulneg1 5417  negdi 5420  divdir 5710  3t3e9 5971  halfpm6th 5979  nneo 6144  ser1add2 6275  ser1add 6276  icoshftf1oi 6342  seq1seqz 6473  seq0seqz 6474  seq01 6484  sqdiv 6548  sumsqne0 6565  binom2 6575  binom2aOLD 6576  discrlem1 6586  nnesq 6592  nn0opthlem1 6594  sqrlem11 6613  sqrlem16 6618  sqrth 6629  sqrmuli 6634  i4 6664  crmul 6671  crrecz 6672  cjcj 6713  readd 6719  imadd 6720  remul 6721  immul 6722  cjadd 6723  cjmul 6724  ipcn 6725  cjmulval 6727  cjneg 6732  addcj 6733  cji 6762  absmul 6782  abs1m 6841  abslem2i 6845  facp1t 6873  fac2 6874  fac3 6875  faclbnd4lem1 6885  bcpasc2 6905  isumnn0nna 7143  0.999... 7181  dfef2 7249  efaddlem5 7284  efaddlem6 7285  efaddlem12 7291  eirrlem3 7332  efsep 7337  eft0val 7339  ef4p 7340  efge1p 7343  efcnlem2 7360  sinadd 7393  cosadd 7394  cos2tOLD 7406  sin01bndlem3 7411  cos2bnd 7417  ruclem15 7467  bcthlem32 7964  ipval2lem1 8285  ipval2 8291  ip0i 8415  ip1ilem 8416  ip2i 8418  ipdirilem 8419  ipasslem10 8430  ip2dii 8435  pythi 8441  siilem1 8442  eulerid 8602  sin2pi 8603  sinperlem1 8605  sincosq3sgn 8623  sincosq4sgn 8624  sincos4thpi 8627  sincos6thpi 8628  hvsubsub4 8847  hvsubcan2 8852  hisubcom 8891  normlem0 8896  normlem1 8897  normlem2 8898  normlem3 8899  normlem6 8902  normlem8 8904  normlem9 8905  bcseq 8907  norm-ii 8925  norm-iii 8927  normpyth 8930  norm3dif 8935  normpar 8942  normpar2 8944  polid2 8945  polid 8946  bcsALT 8967  projlem3 9104  projlem4 9105  pjthlem5 9138  ledir 9375  h1de2 9391  cmcmlem 9451  cmbr2 9456  cm2jt 9480  fh3 9483  fh4 9484  pjadd 9537  pjsslem 9541  pjssm 9543  pjdifnorm 9545  hhlno 9743  lnopeq0lem1 9845  lnopunilem1 9850  lnophmlem2 9857  pjsdi2 9996  pjclem1 10033  golem1 10108  1cat 10536

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-xp 3174  df-cnv 3176  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fv 3188  df-opr 3950

Copyright terms: Public domain