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

Theorem oveq12 6112
Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
Assertion
Ref Expression
oveq12  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 6110 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 6111 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2495 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369  (class class class)co 6103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2733  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-iota 5393  df-fv 5438  df-ov 6106
This theorem is referenced by:  oveq12i  6115  oveq12d  6121  oveqan12d  6122  sprmpt2d  6754  oev2  6975  oa00  7010  omopthi  7108  ecopoveq  7213  ecopovtrn  7215  th3qlem1  7218  th3qlem2  7219  isfsupp  7636  cantnffval  7881  fpwwe2  8822  halfnq  9157  distrlem5pr  9208  addcmpblnr  9251  addsrpr  9254  mulsrpr  9255  ltsrpr  9256  mulgt0sr  9284  add20  9863  msqge0  9873  recextlem2  9979  cru  10326  zaddcl  10697  qaddcl  10981  qmulcl  10983  xaddval  11205  xmulval  11207  xadddilem  11269  fzopth  11507  modval  11722  1exp  11905  nn0opthi  12060  faclbnd  12078  faclbnd3  12080  bcn0  12098  ccatopth  12376  ccatopth2  12377  repswccat  12435  reval  12607  absval  12739  clim  12984  rlim  12985  fsumparts  13281  cpnnen  13523  dvds2add  13576  dvds2sub  13577  gcddvds  13711  gcdcl  13713  gcdeq0  13717  gcdneg  13722  gcdaddmlem  13724  gcdabs  13729  bezoutlem3  13736  bezout  13738  gcddiv  13745  eucalgval2  13768  isprm5  13810  prmexpb  13815  rpexp  13818  rpmul  13821  nn0gcdsq  13842  opoe  13890  omoe  13891  opeo  13892  omeo  13893  pcqmul  13932  prmreclem3  13991  mul4sq  14027  vdwapval  14046  f1ocpbl  14475  homfval  14643  comfval  14651  issect  14704  isfull  14832  isfth  14836  natfval  14868  catchom  14979  catcco  14981  plusfval  15440  isgim  15802  subgga  15830  cayleylem1  15929  lsmsubm  16164  subgdisjb  16202  pj1fval  16203  odadd1  16342  divsabl  16359  cygabl  16379  dprdsubg  16533  dfrhm2  16820  isrhm  16823  isrim0  16825  scafval  16979  lss1d  17056  islmhm  17120  islmim  17155  mplval  17513  mplcoe5lem  17559  opsrval  17568  evlval  17622  mpfind  17634  znfld  18005  cygznlem3  18014  cnmsgnsubg  18019  psgnghm  18022  ipeq0  18079  ipfval  18090  dsmmval  18171  dsmmacl  18178  mavmul0g  18376  marrepfval  18383  marrepeval  18386  marepvfval  18388  marepveval  18391  submafval  18402  submaeval  18405  mdetfval  18409  madugsum  18461  minmar1fval  18464  minmar1eval  18467  symgmatr01  18472  gsummatr01lem3  18475  gsummatr01lem4  18476  gsummatr01  18477  tx2ndc  19236  cnmpt2t  19258  cnmpt22f  19260  hmeofval  19343  divstgplem  19703  stdbdmetval  20101  nmofval  20305  nghmfval  20313  isnmhm  20337  xrsxmet  20398  isphtpy  20565  isphtpc  20578  pcorevlem  20610  cphnm  20724  tchnmval  20756  ipcau2  20761  tchcphlem1  20762  tchcphlem2  20763  tchcph  20764  bcthlem1  20847  bcth  20852  dyadmax  21090  volcn  21098  vitalilem1  21100  vitalilem2  21101  vitalilem3  21102  vitali  21105  i1fmullem  21184  itg1addlem4  21189  dvlip  21477  ftc1a  21521  mdegfval  21543  r1pval  21640  coeaddlem  21728  quotval  21770  elqaalem2  21798  taylfval  21836  cxpcn3  22198  resqrcn  22199  sqrcn  22200  abscxpbnd  22203  angval  22209  chordthmlem  22239  dcubic  22253  lgsdchr  22699  mul2sq  22716  ostthlem2  22889  tglngval  22997  wlkon  23441  wlkonprop  23443  trls  23447  trlon  23451  trlonprop  23453  pths  23477  spths  23478  pthon  23486  pthonprop  23488  spthon  23493  spthonprp  23496  isconngra  23570  isconngra1  23571  ablosn  23846  rngo2  23887  hmoval  24222  htth  24332  normval  24538  hlimi  24602  hsn0elch  24663  ocsh  24698  shscli  24732  shs00i  24865  chj00i  24902  riesz4i  25479  stm1addi  25661  stm1add3i  25663  superpos  25770  metidv  26331  rmulccn  26370  pl1cn  26397  sibfof  26738  subfacval2  27087  m1expevenALT  27119  txsconlem  27141  iscvm  27160  ghomgrpilem2  27317  ghomsn  27319  ismblfin  28444  itg2addnclem3  28457  itg2addnc  28458  ftc1anclem3  28481  ftc1anc  28487  bfp  28735  rngohomco  28792  rngoisoval  28795  rngoisocnv  28799  crngohomfo  28818  keridl  28844  ispridlc  28882  mendval  29552  mendplusg  29555  mulvval  29736  fzoopth  30225  wwlkn  30328  is2wlkonot  30394  is2spthonot  30395  2wlkonot  30396  2spthonot  30397  2wlksot  30398  2spthsot  30399  2wlkonot3v  30406  2spthonot3v  30407  clwlk  30430  clwlkcompim  30439  clwwlkn  30442  clwwlknprop  30447  isrgra  30555  mat1dimcrng  30885  dmatmulcl  30891  scmatsubcl  30896  scmatmulcl  30898  pmatcollpw1lem3  30910  pmatcollpw1  30916  mp2pm2mplem3  30930  mp2pm2mplem4  30931  pmattomply1f1  30934  lincsumcl  30977  bj-bary1  32613  snatpsubN  33406  cdlemn11pre  34867  dihord2pre  34882  baerlem3lem1  35364
  Copyright terms: Public domain W3C validator