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

Theorem oveq12 6205
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 6203 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 6204 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2443 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1399  (class class class)co 6196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504  df-ov 6199
This theorem is referenced by:  oveq12i  6208  oveq12d  6214  oveqan12d  6215  sprmpt2d  6870  oev2  7091  oa00  7126  omopthi  7224  ecopoveq  7330  ecopovtrn  7332  isfsupp  7748  cantnffval  7993  fpwwe2  8932  halfnq  9265  distrlem5pr  9316  addcmpblnr  9357  ltsrpr  9365  mulgt0sr  9393  add20  9982  msqge0  9991  recextlem2  10097  cru  10444  zaddcl  10821  qaddcl  11117  qmulcl  11119  xaddval  11343  xmulval  11345  xadddilem  11407  fzopth  11642  modval  11898  1exp  12098  nn0opthi  12252  faclbnd  12270  faclbnd3  12272  bcn0  12290  ccatopth  12606  ccatopth2  12607  repswccat  12668  reval  12941  absval  13073  clim  13319  rlim  13320  fsumparts  13622  cpnnen  13964  dvds2add  14017  dvds2sub  14018  gcddvds  14155  gcdcl  14157  gcdeq0  14161  gcdneg  14166  gcdaddmlem  14168  gcdabs  14173  bezoutlem3  14180  bezout  14182  gcddiv  14189  eucalgval2  14212  isprm5  14255  prmexpb  14260  rpexp  14263  rpmul  14266  nn0gcdsq  14287  opoe  14337  omoe  14338  opeo  14339  omeo  14340  pcqmul  14379  prmreclem3  14438  mul4sq  14474  vdwapval  14493  f1ocpbl  14932  homfval  15098  comfval  15106  issect  15159  isfull  15316  isfth  15320  natfval  15352  catchom  15495  catcco  15497  funcsetcestrclem5  15545  plusfval  15995  isgim  16427  subgga  16455  cayleylem1  16554  lsmsubm  16790  subgdisjb  16828  pj1fval  16829  odadd1  16971  qusabl  16988  cygabl  17010  dprdsubg  17184  dfrhm2  17479  isrhm  17483  isrim0  17485  scafval  17644  lss1d  17722  islmhm  17786  islmim  17821  mplval  18197  mplcoe5lem  18243  opsrval  18252  evlval  18306  mpfind  18318  znfld  18690  cygznlem3  18699  cnmsgnsubg  18704  psgnghm  18707  ipeq0  18764  ipfval  18775  dsmmval  18856  dsmmacl  18863  mat1dimcrng  19064  dmatval  19079  dmatmulcl  19087  scmatval  19091  scmataddcl  19103  scmatsubcl  19104  scmatmulcl  19105  mavmul0g  19140  marrepfval  19147  marrepeval  19150  marepvfval  19152  marepveval  19155  submafval  19166  submaeval  19169  mdetfval  19173  madugsum  19230  minmar1fval  19233  minmar1eval  19236  symgmatr01  19241  gsummatr01lem3  19244  gsummatr01lem4  19245  gsummatr01  19246  cpmatacl  19302  mat2pmatfval  19309  mat2pmatvalel  19311  mat2pmatmul  19317  cpm2mfval  19335  cpm2mvalel  19337  m2cpminvid  19339  m2cpminvid2  19341  decpmate  19352  pmatcollpw1  19362  monmatcollpw  19365  pmatcollpwlem  19366  pmatcollpw  19367  pmatcollpwscmatlem2  19376  pm2mpval  19381  pm2mpf1  19385  mp2pm2mplem3  19394  mp2pm2mplem4  19395  chpmatfval  19416  tx2ndc  20237  cnmpt2t  20259  cnmpt22f  20261  hmeofval  20344  qustgplem  20704  stdbdmetval  21102  nmofval  21306  nghmfval  21314  isnmhm  21338  xrsxmet  21399  isphtpy  21566  isphtpc  21579  pcorevlem  21611  cphnm  21725  tchnmval  21757  ipcau2  21762  tchcphlem1  21763  tchcphlem2  21764  tchcph  21765  bcthlem1  21848  bcth  21853  dyadmax  22092  volcn  22100  vitalilem1  22102  vitalilem2  22103  vitalilem3  22104  vitali  22107  i1fmullem  22186  itg1addlem4  22191  dvlip  22479  ftc1a  22523  mdegfval  22545  r1pval  22642  coeaddlem  22731  quotval  22773  elqaalem2  22801  taylfval  22839  cxpcn3  23209  resqrtcn  23210  sqrtcn  23211  abscxpbnd  23214  angval  23251  chordthmlem  23279  dcubic  23293  lgsdchr  23740  mul2sq  23757  ostthlem2  23930  tglngval  24058  ishpg  24248  wlkon  24654  wlkonprop  24656  trls  24659  trlon  24663  trlonprop  24665  pths  24689  spths  24690  pthon  24698  pthonprop  24700  spthon  24705  spthonprp  24708  isconngra  24793  isconngra1  24794  wwlkn  24803  clwlk  24874  clwlkcompim  24885  clwwlkn  24888  clwwlknprop  24893  is2wlkonot  24984  is2spthonot  24985  2wlkonot  24986  2spthonot  24987  2wlksot  24988  2spthsot  24989  2wlkonot3v  24996  2spthonot3v  24997  isrgra  25047  ablosn  25466  rngo2  25507  hmoval  25842  htth  25952  normval  26158  hlimi  26222  hsn0elch  26283  ocsh  26318  shscli  26352  shs00i  26485  chj00i  26522  riesz4i  27098  stm1addi  27280  stm1add3i  27282  superpos  27389  metidv  28025  rmulccn  28064  pl1cn  28091  sibfof  28465  subfacval2  28820  m1expevenALT  28852  txsconlem  28874  iscvm  28893  ghomgrpilem2  29215  ghomsn  29217  ismblfin  30220  itg2addnclem3  30234  itg2addnc  30235  ftc1anclem3  30258  ftc1anc  30264  bfp  30486  rngohomco  30543  rngoisoval  30546  rngoisocnv  30550  crngohomfo  30569  keridl  30595  ispridlc  30633  mendval  31300  mendplusg  31303  lcmabs  31379  mulvval  31545  climf  31794  cxpcncf2  31869  opoeALTV  32525  opeoALTV  32526  fzoopth  32660  rnghmval  32897  isrngisom  32902  rhmval  32925  rngchomALTV  32993  funcrngcsetcALT  33007  funcringcsetcALTV2lem5  33048  ringchomALTV  33056  funcringcsetclem5ALTV  33071  srhmsubclem3  33083  srhmsubc  33084  fldhmsubc  33092  srhmsubcALTVlem3  33102  srhmsubcALTV  33103  fldhmsubcALTV  33111  dmatALTval  33201  lincsumcl  33232  fdivval  33360  bj-bary1  35025  snatpsubN  35887  cdlemn11pre  37350  dihord2pre  37365  baerlem3lem1  37847
  Copyright terms: Public domain W3C validator