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

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

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 7146 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2 oveq2 7147 . 2 (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
31, 2sylan9eq 2856 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  (class class class)co 7139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142
This theorem is referenced by:  oveq12i  7151  oveq12d  7157  oveqan12d  7158  mptmpoopabovd  7766  suppofssd  7854  sprmpod  7877  oev2  8135  oa00  8172  omopthi  8271  ecopoveq  8385  ecopovtrn  8387  isfsupp  8825  cantnffval  9114  fpwwe2  10058  halfnq  10391  distrlem5pr  10442  addcmpblnr  10484  ltsrpr  10492  mulgt0sr  10520  add20  11145  msqge0  11154  recextlem2  11264  cru  11621  zaddcl  12014  qaddcl  12356  qmulcl  12358  xaddval  12608  xmulval  12610  xnn0xadd0  12632  xadddilem  12679  fzopth  12943  modval  13238  1exp  13458  m1expeven  13476  nn0opthi  13630  faclbnd  13650  faclbnd3  13652  bcn0  13670  ccatopth  14073  ccatopth2  14074  repswccat  14143  reval  14460  absval  14592  clim  14846  rlim  14847  fsumparts  15156  cpnnen  15577  dvds2add  15638  dvds2sub  15639  opoe  15707  omoe  15708  opeo  15709  omeo  15710  gcddvds  15845  gcdcl  15848  gcdeq0  15858  gcdneg  15863  gcdaddmlem  15865  gcdabs  15870  bezoutlem3  15882  bezout  15884  gcddiv  15892  eucalgval2  15918  lcmabs  15942  rpmul  15996  divgcdcoprmex  16003  isprm5  16044  prmexpb  16055  rpexp  16057  nn0gcdsq  16085  pcqmul  16183  prmreclem3  16247  mul4sq  16283  vdwapval  16302  f1ocpbl  16793  homfval  16957  comfval  16965  issect  17018  isfull  17175  isfth  17179  natfval  17211  catchom  17354  catcco  17356  funcsetcestrclem5  17404  plusfval  17854  0subm  17977  cycsubm  18340  cyccom  18341  isgim  18397  subgga  18425  cayleylem1  18535  lsmsubm  18773  subgdisjb  18814  pj1fval  18815  odadd1  18964  qusabl  18981  cygablOLD  19007  dprdsubg  19142  ringadd2  19324  dfrhm2  19468  isrhm  19472  isrim0  19474  scafval  19649  rmodislmodlem  19697  rmodislmod  19698  lss1d  19731  islmhm  19795  islmim  19830  znfld  20255  cygznlem3  20264  cnmsgnsubg  20269  psgnghm  20272  ipeq0  20330  ipfval  20341  dsmmval  20426  dsmmacl  20433  mplval  20669  mplcoe5lem  20710  opsrval  20717  evlval  20770  mpfind  20782  selvffval  20791  mhpfval  20794  mat1dimcrng  21085  dmatval  21100  dmatmulcl  21108  scmatval  21112  scmataddcl  21124  scmatsubcl  21125  scmatmulcl  21126  mavmul0g  21161  marrepfval  21168  marrepeval  21171  marepvfval  21173  marepveval  21176  submafval  21187  submaeval  21190  mdetfval  21194  madugsum  21251  minmar1fval  21254  minmar1eval  21257  symgmatr01  21262  gsummatr01lem3  21265  gsummatr01lem4  21266  gsummatr01  21267  cpmatacl  21324  mat2pmatfval  21331  mat2pmatvalel  21333  mat2pmatmul  21339  cpm2mfval  21357  cpm2mvalel  21359  m2cpminvid  21361  m2cpminvid2  21363  decpmate  21374  pmatcollpw1  21384  monmatcollpw  21387  pmatcollpwlem  21388  pmatcollpw  21389  pmatcollpwscmatlem2  21398  pm2mpval  21403  pm2mpf1  21407  mp2pm2mplem3  21416  mp2pm2mplem4  21417  chpmatfval  21438  tx2ndc  22259  cnmpt2t  22281  cnmpt22f  22283  hmeofval  22366  qustgplem  22729  stdbdmetval  23124  nmofval  23323  nghmfval  23331  isnmhm  23355  xrsxmet  23417  isphtpy  23589  isphtpc  23602  pcorevlem  23634  cphnm  23801  tcphnmval  23836  ipcau2  23841  tcphcphlem1  23842  tcphcphlem2  23843  tcphcph  23844  bcthlem1  23931  bcth  23936  dyadmax  24205  volcn  24213  vitalilem1  24215  vitalilem2  24216  vitalilem3  24217  vitali  24220  i1fmullem  24301  itg1addlem4  24306  dvlip  24599  ftc1a  24643  mdegfval  24666  r1pval  24760  coeaddlem  24849  quotval  24891  elqaalem2  24919  taylfval  24957  cxpcn3  25340  resqrtcn  25341  sqrtcn  25342  abscxpbnd  25345  angval  25390  chordthmlem  25421  dcubic  25435  lgsdchr  25942  mul2sq  26006  ostthlem2  26215  tglngval  26348  islnopp  26536  ishpg  26556  finsumvtxdg2size  27343  wspthsn  27637  wwlksnon  27640  wspthsnon  27641  iswspthsnon  27645  2clwwlk  28135  numclwlk1lem2  28158  numclwwlkovh0  28160  hmoval  28596  htth  28704  normval  28910  hlimi  28974  hsn0elch  29034  ocsh  29069  shscli  29103  shs00i  29236  chj00i  29273  riesz4i  29849  stm1addi  30031  stm1add3i  30033  superpos  30140  prmidlc  31032  idlsrgmulrval  31062  brfinext  31131  submateq  31162  metidv  31243  rmulccn  31279  pl1cn  31306  sibfof  31706  cxpcncf1  31974  subfacval2  32542  txsconnlem  32595  iscvm  32614  prv  32783  bj-bary1  34721  ismblfin  35091  itg2addnclem3  35103  itg2addnc  35104  ftc1anclem3  35125  ftc1anc  35131  bfp  35255  rngo2  35338  rngohomco  35405  rngoisoval  35408  rngoisocnv  35412  crngohomfo  35437  keridl  35463  ispridlc  35501  snatpsubN  37039  cdlemn11pre  38499  dihord2pre  38514  baerlem3lem1  38996  nn0rppwr  39477  sn-inelr  39577  mendval  40114  mendplusg  40117  mulvval  41159  climf  42251  climf2  42295  cxpcncf2  42528  smflimlem3  43393  fzoopth  43871  fmtnofac2lem  44072  prmdvdsfmtnof1lem2  44089  opoeALTV  44188  opeoALTV  44189  rnghmval  44502  isrngisom  44507  rhmval  44530  rngchomALTV  44596  funcrngcsetcALT  44610  funcringcsetcALTV2lem5  44651  ringchomALTV  44659  funcringcsetclem5ALTV  44674  srhmsubclem3  44686  srhmsubc  44687  fldhmsubc  44695  srhmsubcALTVlem2  44704  srhmsubcALTV  44705  fldhmsubcALTV  44713  dmatALTval  44796  lincsumcl  44827  fdivval  44940
  Copyright terms: Public domain W3C validator