MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveq12 Structured version   Visualization version   GIF version

Theorem oveq12 6893
Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
Assertion
Ref Expression
oveq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 6891 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2 oveq2 6892 . 2 (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
31, 2sylan9eq 2871 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  (class class class)co 6884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-iota 6074  df-fv 6119  df-ov 6887
This theorem is referenced by:  oveq12i  6896  oveq12d  6902  oveqan12d  6903  mptmpt2opabovd  7492  sprmpt2d  7595  oev2  7850  oa00  7886  omopthi  7984  ecopoveq  8094  ecopovtrn  8096  isfsupp  8528  cantnffval  8817  fpwwe2  9760  halfnq  10093  distrlem5pr  10144  addcmpblnr  10185  ltsrpr  10193  mulgt0sr  10221  add20  10835  msqge0  10844  recextlem2  10953  cru  11307  zaddcl  11703  qaddcl  12043  qmulcl  12045  xaddval  12292  xmulval  12294  xnn0xadd0  12315  xadddilem  12362  fzopth  12621  modval  12914  1exp  13132  m1expeven  13150  nn0opthi  13297  faclbnd  13317  faclbnd3  13319  bcn0  13337  ccatopth  13714  ccatopth2  13715  repswccat  13776  reval  14089  absval  14221  clim  14468  rlim  14469  fsumparts  14780  cpnnen  15198  dvds2add  15258  dvds2sub  15259  opoe  15327  omoe  15328  opeo  15329  omeo  15330  gcddvds  15464  gcdcl  15467  gcdeq0  15477  gcdneg  15482  gcdaddmlem  15484  gcdabs  15489  bezoutlem3  15497  bezout  15499  gcddiv  15507  eucalgval2  15533  lcmabs  15557  rpmul  15611  divgcdcoprmex  15618  isprm5  15656  prmexpb  15667  rpexp  15669  nn0gcdsq  15697  pcqmul  15795  prmreclem3  15859  mul4sq  15895  vdwapval  15914  f1ocpbl  16410  homfval  16576  comfval  16584  issect  16637  isfull  16794  isfth  16798  natfval  16830  catchom  16973  catcco  16975  funcsetcestrclem5  17024  plusfval  17473  isgim  17926  subgga  17954  cayleylem1  18053  lsmsubm  18289  subgdisjb  18327  pj1fval  18328  odadd1  18472  qusabl  18489  cygabl  18513  dprdsubg  18645  ringadd2  18797  dfrhm2  18941  isrhm  18945  isrim0  18947  scafval  19106  rmodislmodlem  19154  rmodislmod  19155  lss1d  19190  islmhm  19254  islmim  19289  mplval  19657  mplcoe5lem  19696  opsrval  19703  evlval  19752  mpfind  19764  znfld  20136  cygznlem3  20145  cnmsgnsubg  20150  psgnghm  20153  ipeq0  20213  ipfval  20224  dsmmval  20309  dsmmacl  20316  mat1dimcrng  20515  dmatval  20530  dmatmulcl  20538  scmatval  20542  scmataddcl  20554  scmatsubcl  20555  scmatmulcl  20556  mavmul0g  20591  marrepfval  20598  marrepeval  20601  marepvfval  20603  marepveval  20606  submafval  20617  submaeval  20620  mdetfval  20624  madugsum  20681  minmar1fval  20684  minmar1eval  20687  symgmatr01  20693  gsummatr01lem3  20696  gsummatr01lem4  20697  gsummatr01  20698  cpmatacl  20755  mat2pmatfval  20762  mat2pmatvalel  20764  mat2pmatmul  20770  cpm2mfval  20788  cpm2mvalel  20790  m2cpminvid  20792  m2cpminvid2  20794  decpmate  20805  pmatcollpw1  20815  monmatcollpw  20818  pmatcollpwlem  20819  pmatcollpw  20820  pmatcollpwscmatlem2  20829  pm2mpval  20834  pm2mpf1  20838  mp2pm2mplem3  20847  mp2pm2mplem4  20848  chpmatfval  20869  tx2ndc  21689  cnmpt2t  21711  cnmpt22f  21713  hmeofval  21796  qustgplem  22158  stdbdmetval  22553  nmofval  22752  nghmfval  22760  isnmhm  22784  xrsxmet  22846  isphtpy  23014  isphtpc  23027  pcorevlem  23059  cphnm  23226  tchnmval  23261  ipcau2  23266  tchcphlem1  23267  tchcphlem2  23268  tchcph  23269  bcthlem1  23355  bcth  23360  dyadmax  23602  volcn  23610  vitalilem1  23612  vitalilem2  23613  vitalilem3  23614  vitali  23617  i1fmullem  23698  itg1addlem4  23703  dvlip  23993  ftc1a  24037  mdegfval  24059  r1pval  24153  coeaddlem  24242  quotval  24284  elqaalem2  24312  taylfval  24350  cxpcn3  24726  resqrtcn  24727  sqrtcn  24728  abscxpbnd  24731  angval  24768  chordthmlem  24796  dcubic  24810  lgsdchr  25317  mul2sq  25381  ostthlem2  25554  tglngval  25683  islnopp  25868  ishpg  25888  finsumvtxdg2size  26697  wspthsn  26993  wwlksnon  26996  wspthsnon  26997  iswspthsnon  27002  iswspthsnonOLD  27003  2clwwlk  27547  numclwlk1lem2  27573  numclwwlkovh0  27575  hmoval  28016  htth  28126  normval  28332  hlimi  28396  hsn0elch  28456  ocsh  28493  shscli  28527  shs00i  28660  chj00i  28697  riesz4i  29273  stm1addi  29455  stm1add3i  29457  superpos  29564  submateq  30223  metidv  30283  rmulccn  30322  pl1cn  30349  sibfof  30750  cxpcncf1  31021  subfacval2  31514  txsconnlem  31567  iscvm  31586  bj-bary1  33498  ismblfin  33782  itg2addnclem3  33794  itg2addnc  33795  ftc1anclem3  33818  ftc1anc  33824  bfp  33953  rngo2  34036  rngohomco  34103  rngoisoval  34106  rngoisocnv  34110  crngohomfo  34135  keridl  34161  ispridlc  34199  snatpsubN  35549  cdlemn11pre  37009  dihord2pre  37024  baerlem3lem1  37506  mendval  38272  mendplusg  38275  mulvval  39188  climf  40352  climf2  40396  cxpcncf2  40611  smflimlem3  41481  fzoopth  41930  fmtnofac2lem  42073  prmdvdsfmtnof1lem2  42090  opoeALTV  42187  opeoALTV  42188  rnghmval  42477  isrngisom  42482  rhmval  42505  rngchomALTV  42571  funcrngcsetcALT  42585  funcringcsetcALTV2lem5  42626  ringchomALTV  42634  funcringcsetclem5ALTV  42649  srhmsubclem3  42661  srhmsubc  42662  fldhmsubc  42670  srhmsubcALTVlem2  42679  srhmsubcALTV  42680  fldhmsubcALTV  42688  dmatALTval  42775  lincsumcl  42806  fdivval  42919
  Copyright terms: Public domain W3C validator