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

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

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 6534 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2 oveq2 6535 . 2 (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
31, 2sylan9eq 2664 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  (class class class)co 6527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-iota 5754  df-fv 5798  df-ov 6530
This theorem is referenced by:  oveq12i  6539  oveq12d  6545  oveqan12d  6546  sprmpt2d  7215  oev2  7468  oa00  7504  omopthi  7602  ecopoveq  7713  ecopovtrn  7715  isfsupp  8140  cantnffval  8421  fpwwe2  9322  halfnq  9655  distrlem5pr  9706  addcmpblnr  9747  ltsrpr  9755  mulgt0sr  9783  add20  10392  msqge0  10401  recextlem2  10510  cru  10862  zaddcl  11253  qaddcl  11639  qmulcl  11641  xaddval  11890  xmulval  11892  xadddilem  11956  fzopth  12207  modval  12490  1exp  12709  m1expeven  12727  nn0opthi  12877  faclbnd  12897  faclbnd3  12899  bcn0  12917  ccatopth  13271  ccatopth2  13272  repswccat  13332  reval  13643  absval  13775  clim  14022  rlim  14023  fsumparts  14328  cpnnen  14746  dvds2add  14802  dvds2sub  14803  opoe  14874  omoe  14875  opeo  14876  omeo  14877  gcddvds  15012  gcdcl  15015  gcdeq0  15025  gcdneg  15030  gcdaddmlem  15032  gcdabs  15037  bezoutlem3  15045  bezout  15047  gcddiv  15055  eucalgval2  15081  lcmabs  15105  rpmul  15160  divgcdcoprmex  15167  isprm5  15206  prmexpb  15217  rpexp  15219  nn0gcdsq  15247  pcqmul  15345  prmreclem3  15409  mul4sq  15445  vdwapval  15464  f1ocpbl  15957  homfval  16124  comfval  16132  issect  16185  isfull  16342  isfth  16346  natfval  16378  catchom  16521  catcco  16523  funcsetcestrclem5  16571  plusfval  17020  isgim  17476  subgga  17505  cayleylem1  17604  lsmsubm  17840  subgdisjb  17878  pj1fval  17879  odadd1  18023  qusabl  18040  cygabl  18064  dprdsubg  18195  ringadd2  18347  dfrhm2  18489  isrhm  18493  isrim0  18495  scafval  18654  lss1d  18733  islmhm  18797  islmim  18832  mplval  19198  mplcoe5lem  19237  opsrval  19244  evlval  19294  mpfind  19306  znfld  19676  cygznlem3  19685  cnmsgnsubg  19690  psgnghm  19693  ipeq0  19750  ipfval  19761  dsmmval  19845  dsmmacl  19852  mat1dimcrng  20050  dmatval  20065  dmatmulcl  20073  scmatval  20077  scmataddcl  20089  scmatsubcl  20090  scmatmulcl  20091  mavmul0g  20126  marrepfval  20133  marrepeval  20136  marepvfval  20138  marepveval  20141  submafval  20152  submaeval  20155  mdetfval  20159  madugsum  20216  minmar1fval  20219  minmar1eval  20222  symgmatr01  20227  gsummatr01lem3  20230  gsummatr01lem4  20231  gsummatr01  20232  cpmatacl  20288  mat2pmatfval  20295  mat2pmatvalel  20297  mat2pmatmul  20303  cpm2mfval  20321  cpm2mvalel  20323  m2cpminvid  20325  m2cpminvid2  20327  decpmate  20338  pmatcollpw1  20348  monmatcollpw  20351  pmatcollpwlem  20352  pmatcollpw  20353  pmatcollpwscmatlem2  20362  pm2mpval  20367  pm2mpf1  20371  mp2pm2mplem3  20380  mp2pm2mplem4  20381  chpmatfval  20402  tx2ndc  21212  cnmpt2t  21234  cnmpt22f  21236  hmeofval  21319  qustgplem  21682  stdbdmetval  22077  nmofval  22276  nghmfval  22284  isnmhm  22308  xrsxmet  22368  isphtpy  22536  isphtpc  22549  pcorevlem  22582  cphnm  22746  tchnmval  22781  ipcau2  22786  tchcphlem1  22787  tchcphlem2  22788  tchcph  22789  bcthlem1  22874  bcth  22879  dyadmax  23117  volcn  23125  vitalilem1  23127  vitalilem1OLD  23128  vitalilem2  23129  vitalilem3  23130  vitali  23133  i1fmullem  23212  itg1addlem4  23217  dvlip  23505  ftc1a  23549  mdegfval  23571  r1pval  23665  coeaddlem  23754  quotval  23796  elqaalem2  23824  taylfval  23862  cxpcn3  24234  resqrtcn  24235  sqrtcn  24236  abscxpbnd  24239  angval  24276  chordthmlem  24304  dcubic  24318  lgsdchr  24825  mul2sq  24889  ostthlem2  25062  tglngval  25192  islnopp  25377  ishpg  25397  wlkon  25855  wlkonprop  25857  trls  25860  trlon  25864  trlonprop  25866  pths  25890  spths  25891  pthon  25899  pthonprop  25901  spthon  25906  spthonprp  25909  isconngra  25994  isconngra1  25995  wwlkn  26004  clwlk  26075  clwlkcompim  26086  clwwlkn  26089  clwwlknprop  26094  is2wlkonot  26184  is2spthonot  26185  2wlkonot  26186  2spthonot  26187  2wlksot  26188  2spthsot  26189  2wlkonot3v  26196  2spthonot3v  26197  isrgra  26247  hmoval  26843  htth  26953  normval  27159  hlimi  27223  hsn0elch  27283  ocsh  27320  shscli  27354  shs00i  27487  chj00i  27524  riesz4i  28100  stm1addi  28282  stm1add3i  28284  superpos  28391  submateq  28997  metidv  29057  rmulccn  29096  pl1cn  29123  sibfof  29523  subfacval2  30217  txsconlem  30270  iscvm  30289  bj-bary1  32133  ismblfin  32414  itg2addnclem3  32427  itg2addnc  32428  ftc1anclem3  32451  ftc1anc  32457  bfp  32587  rngo2  32670  rngohomco  32737  rngoisoval  32740  rngoisocnv  32744  crngohomfo  32769  keridl  32795  ispridlc  32833  snatpsubN  33848  cdlemn11pre  35311  dihord2pre  35326  baerlem3lem1  35808  mendval  36566  mendplusg  36569  mulvval  37487  climf  38483  climf2  38527  cxpcncf2  38580  smflimlem3  39453  fmtnofac2lem  39813  prmdvdsfmtnof1lem2  39830  opoeALTV  39927  opeoALTV  39928  mptmpt2opabovd  40153  fzoopth  40177  xnn0xadd0  40207  wspthsn  41038  wwlksnon  41041  wspthsnon  41042  iswspthsnon  41044  rnghmval  41673  isrngisom  41678  rhmval  41701  rngchomALTV  41769  funcrngcsetcALT  41783  funcringcsetcALTV2lem5  41824  ringchomALTV  41832  funcringcsetclem5ALTV  41847  srhmsubclem3  41859  srhmsubc  41860  fldhmsubc  41868  srhmsubcALTVlem3  41878  srhmsubcALTV  41879  fldhmsubcALTV  41887  dmatALTval  41975  lincsumcl  42006  fdivval  42123
  Copyright terms: Public domain W3C validator