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

Theorem oveq12 6314
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 6312 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 6313 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2490 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437  (class class class)co 6305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308
This theorem is referenced by:  oveq12i  6317  oveq12d  6323  oveqan12d  6324  sprmpt2d  6978  oev2  7233  oa00  7268  omopthi  7366  ecopoveq  7472  ecopovtrn  7474  isfsupp  7893  cantnffval  8167  fpwwe2  9067  halfnq  9400  distrlem5pr  9451  addcmpblnr  9492  ltsrpr  9500  mulgt0sr  9528  add20  10125  msqge0  10134  recextlem2  10242  cru  10601  zaddcl  10977  qaddcl  11280  qmulcl  11282  xaddval  11516  xmulval  11518  xadddilem  11580  fzopth  11833  modval  12095  1exp  12298  m1expeven  12316  nn0opthi  12453  faclbnd  12472  faclbnd3  12474  bcn0  12492  ccatopth  12811  ccatopth2  12812  repswccat  12873  reval  13148  absval  13280  clim  13536  rlim  13537  fsumparts  13844  cpnnen  14259  dvds2add  14312  dvds2sub  14313  gcddvds  14451  gcdcl  14454  gcdeq0  14459  gcdneg  14464  gcdaddmlem  14466  gcdabs  14471  bezoutlem3  14479  bezout  14481  gcddiv  14488  eucalgval2  14511  lcmabs  14535  isprm5  14613  prmexpb  14632  rpexp  14634  rpmul  14637  nn0gcdsq  14663  opoe  14715  omoe  14716  opeo  14717  omeo  14718  pcqmul  14757  prmreclem3  14816  mul4sq  14852  vdwapval  14877  f1ocpbl  15373  homfval  15539  comfval  15547  issect  15600  isfull  15757  isfth  15761  natfval  15793  catchom  15936  catcco  15938  funcsetcestrclem5  15986  plusfval  16436  isgim  16868  subgga  16896  cayleylem1  16995  lsmsubm  17231  subgdisjb  17269  pj1fval  17270  odadd1  17412  qusabl  17429  cygabl  17451  dprdsubg  17583  dfrhm2  17871  isrhm  17875  isrim0  17877  scafval  18036  lss1d  18112  islmhm  18176  islmim  18211  mplval  18578  mplcoe5lem  18617  opsrval  18624  evlval  18673  mpfind  18685  znfld  19053  cygznlem3  19062  cnmsgnsubg  19067  psgnghm  19070  ipeq0  19127  ipfval  19138  dsmmval  19219  dsmmacl  19226  mat1dimcrng  19424  dmatval  19439  dmatmulcl  19447  scmatval  19451  scmataddcl  19463  scmatsubcl  19464  scmatmulcl  19465  mavmul0g  19500  marrepfval  19507  marrepeval  19510  marepvfval  19512  marepveval  19515  submafval  19526  submaeval  19529  mdetfval  19533  madugsum  19590  minmar1fval  19593  minmar1eval  19596  symgmatr01  19601  gsummatr01lem3  19604  gsummatr01lem4  19605  gsummatr01  19606  cpmatacl  19662  mat2pmatfval  19669  mat2pmatvalel  19671  mat2pmatmul  19677  cpm2mfval  19695  cpm2mvalel  19697  m2cpminvid  19699  m2cpminvid2  19701  decpmate  19712  pmatcollpw1  19722  monmatcollpw  19725  pmatcollpwlem  19726  pmatcollpw  19727  pmatcollpwscmatlem2  19736  pm2mpval  19741  pm2mpf1  19745  mp2pm2mplem3  19754  mp2pm2mplem4  19755  chpmatfval  19776  tx2ndc  20588  cnmpt2t  20610  cnmpt22f  20612  hmeofval  20695  qustgplem  21057  stdbdmetval  21451  nmofval  21637  nghmfval  21645  isnmhm  21669  xrsxmet  21729  isphtpy  21896  isphtpc  21909  pcorevlem  21941  cphnm  22055  tchnmval  22087  ipcau2  22092  tchcphlem1  22093  tchcphlem2  22094  tchcph  22095  bcthlem1  22176  bcth  22181  dyadmax  22424  volcn  22432  vitalilem1  22434  vitalilem2  22435  vitalilem3  22436  vitali  22439  i1fmullem  22520  itg1addlem4  22525  dvlip  22813  ftc1a  22857  mdegfval  22879  r1pval  22973  coeaddlem  23062  quotval  23104  elqaalem2  23132  taylfval  23170  cxpcn3  23544  resqrtcn  23545  sqrtcn  23546  abscxpbnd  23549  angval  23586  chordthmlem  23614  dcubic  23628  lgsdchr  24130  mul2sq  24147  ostthlem2  24320  tglngval  24447  islnopp  24629  ishpg  24648  wlkon  25097  wlkonprop  25099  trls  25102  trlon  25106  trlonprop  25108  pths  25132  spths  25133  pthon  25141  pthonprop  25143  spthon  25148  spthonprp  25151  isconngra  25236  isconngra1  25237  wwlkn  25246  clwlk  25317  clwlkcompim  25328  clwwlkn  25331  clwwlknprop  25336  is2wlkonot  25427  is2spthonot  25428  2wlkonot  25429  2spthonot  25430  2wlksot  25431  2spthsot  25432  2wlkonot3v  25439  2spthonot3v  25440  isrgra  25490  ablosn  25911  rngo2  25952  hmoval  26287  htth  26397  normval  26603  hlimi  26667  hsn0elch  26727  ocsh  26762  shscli  26796  shs00i  26929  chj00i  26966  riesz4i  27542  stm1addi  27724  stm1add3i  27726  superpos  27833  submateq  28465  metidv  28525  rmulccn  28564  pl1cn  28591  sibfof  28992  subfacval2  29689  txsconlem  29742  iscvm  29761  ghomgrpilem2  30083  ghomsn  30085  bj-bary1  31453  ismblfin  31675  itg2addnclem3  31689  itg2addnc  31690  ftc1anclem3  31713  ftc1anc  31719  bfp  31850  rngohomco  31907  rngoisoval  31910  rngoisocnv  31914  crngohomfo  31933  keridl  31959  ispridlc  31997  snatpsubN  33014  cdlemn11pre  34477  dihord2pre  34492  baerlem3lem1  34974  mendval  35738  mendplusg  35741  mulvval  36448  climf  37264  cxpcncf2  37340  opoeALTV  38192  opeoALTV  38193  fzoopth  38402  rnghmval  38639  isrngisom  38644  rhmval  38667  rngchomALTV  38735  funcrngcsetcALT  38749  funcringcsetcALTV2lem5  38790  ringchomALTV  38798  funcringcsetclem5ALTV  38813  srhmsubclem3  38825  srhmsubc  38826  fldhmsubc  38834  srhmsubcALTVlem3  38844  srhmsubcALTV  38845  fldhmsubcALTV  38853  dmatALTval  38943  lincsumcl  38974  fdivval  39101
  Copyright terms: Public domain W3C validator