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 2483 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 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-iota 5565  df-fv 5609  df-ov 6308
This theorem is referenced by:  oveq12i  6317  oveq12d  6323  oveqan12d  6324  sprmpt2d  6981  oev2  7236  oa00  7271  omopthi  7369  ecopoveq  7475  ecopovtrn  7477  isfsupp  7896  cantnffval  8176  fpwwe2  9075  halfnq  9408  distrlem5pr  9459  addcmpblnr  9500  ltsrpr  9508  mulgt0sr  9536  add20  10133  msqge0  10142  recextlem2  10250  cru  10608  zaddcl  10984  qaddcl  11287  qmulcl  11289  xaddval  11523  xmulval  11525  xadddilem  11587  fzopth  11842  modval  12104  1exp  12307  m1expeven  12325  nn0opthi  12462  faclbnd  12481  faclbnd3  12483  bcn0  12501  ccatopth  12828  ccatopth2  12829  repswccat  12890  reval  13169  absval  13301  clim  13557  rlim  13558  fsumparts  13865  cpnnen  14280  dvds2add  14333  dvds2sub  14334  gcddvds  14476  gcdcl  14479  gcdeq0  14484  gcdneg  14489  gcdaddmlem  14491  gcdabs  14496  bezoutlem3OLD  14504  bezoutlem3  14507  bezout  14509  gcddiv  14516  eucalgval2  14539  lcmabs  14569  isprm5  14650  prmexpb  14669  rpexp  14671  rpmul  14674  nn0gcdsq  14700  opoe  14760  omoe  14761  opeo  14762  omeo  14763  pcqmul  14802  prmreclem3  14861  mul4sq  14897  vdwapval  14922  f1ocpbl  15430  homfval  15596  comfval  15604  issect  15657  isfull  15814  isfth  15818  natfval  15850  catchom  15993  catcco  15995  funcsetcestrclem5  16043  plusfval  16493  isgim  16925  subgga  16953  cayleylem1  17052  lsmsubm  17304  subgdisjb  17342  pj1fval  17343  odadd1  17485  qusabl  17502  cygabl  17524  dprdsubg  17656  dfrhm2  17944  isrhm  17948  isrim0  17950  scafval  18109  lss1d  18185  islmhm  18249  islmim  18284  mplval  18651  mplcoe5lem  18690  opsrval  18697  evlval  18746  mpfind  18758  znfld  19129  cygznlem3  19138  cnmsgnsubg  19143  psgnghm  19146  ipeq0  19203  ipfval  19214  dsmmval  19295  dsmmacl  19302  mat1dimcrng  19500  dmatval  19515  dmatmulcl  19523  scmatval  19527  scmataddcl  19539  scmatsubcl  19540  scmatmulcl  19541  mavmul0g  19576  marrepfval  19583  marrepeval  19586  marepvfval  19588  marepveval  19591  submafval  19602  submaeval  19605  mdetfval  19609  madugsum  19666  minmar1fval  19669  minmar1eval  19672  symgmatr01  19677  gsummatr01lem3  19680  gsummatr01lem4  19681  gsummatr01  19682  cpmatacl  19738  mat2pmatfval  19745  mat2pmatvalel  19747  mat2pmatmul  19753  cpm2mfval  19771  cpm2mvalel  19773  m2cpminvid  19775  m2cpminvid2  19777  decpmate  19788  pmatcollpw1  19798  monmatcollpw  19801  pmatcollpwlem  19802  pmatcollpw  19803  pmatcollpwscmatlem2  19812  pm2mpval  19817  pm2mpf1  19821  mp2pm2mplem3  19830  mp2pm2mplem4  19831  chpmatfval  19852  tx2ndc  20664  cnmpt2t  20686  cnmpt22f  20688  hmeofval  20771  qustgplem  21133  stdbdmetval  21527  nmofval  21717  nghmfval  21725  nmofvalOLD  21736  nghmfvalOLD  21743  isnmhm  21765  xrsxmet  21825  isphtpy  22010  isphtpc  22023  pcorevlem  22055  cphnm  22169  tchnmval  22201  ipcau2  22206  tchcphlem1  22207  tchcphlem2  22208  tchcph  22209  bcthlem1  22290  bcth  22295  dyadmax  22554  volcn  22562  vitalilem1  22564  vitalilem2  22565  vitalilem3  22566  vitali  22569  i1fmullem  22650  itg1addlem4  22655  dvlip  22943  ftc1a  22987  mdegfval  23009  r1pval  23105  coeaddlem  23201  quotval  23243  elqaalem2  23271  elqaalem2OLD  23274  taylfval  23312  cxpcn3  23686  resqrtcn  23687  sqrtcn  23688  abscxpbnd  23691  angval  23728  chordthmlem  23756  dcubic  23770  lgsdchr  24274  mul2sq  24291  ostthlem2  24464  tglngval  24594  islnopp  24779  ishpg  24799  wlkon  25259  wlkonprop  25261  trls  25264  trlon  25268  trlonprop  25270  pths  25294  spths  25295  pthon  25303  pthonprop  25305  spthon  25310  spthonprp  25313  isconngra  25398  isconngra1  25399  wwlkn  25408  clwlk  25479  clwlkcompim  25490  clwwlkn  25493  clwwlknprop  25498  is2wlkonot  25589  is2spthonot  25590  2wlkonot  25591  2spthonot  25592  2wlksot  25593  2spthsot  25594  2wlkonot3v  25601  2spthonot3v  25602  isrgra  25652  ablosn  26073  rngo2  26114  hmoval  26449  htth  26569  normval  26775  hlimi  26839  hsn0elch  26899  ocsh  26934  shscli  26968  shs00i  27101  chj00i  27138  riesz4i  27714  stm1addi  27896  stm1add3i  27898  superpos  28005  submateq  28643  metidv  28703  rmulccn  28742  pl1cn  28769  sibfof  29181  subfacval2  29918  txsconlem  29971  iscvm  29990  ghomgrpilem2  30312  ghomsn  30314  bj-bary1  31681  ismblfin  31945  itg2addnclem3  31959  itg2addnc  31960  ftc1anclem3  31983  ftc1anc  31989  bfp  32120  rngohomco  32177  rngoisoval  32180  rngoisocnv  32184  crngohomfo  32203  keridl  32229  ispridlc  32267  snatpsubN  33284  cdlemn11pre  34747  dihord2pre  34762  baerlem3lem1  35244  mendval  36019  mendplusg  36022  mulvval  36791  climf  37642  cxpcncf2  37718  opoeALTV  38682  opeoALTV  38683  fzoopth  38917  rnghmval  39510  isrngisom  39515  rhmval  39538  rngchomALTV  39606  funcrngcsetcALT  39620  funcringcsetcALTV2lem5  39661  ringchomALTV  39669  funcringcsetclem5ALTV  39684  srhmsubclem3  39696  srhmsubc  39697  fldhmsubc  39705  srhmsubcALTVlem3  39715  srhmsubcALTV  39716  fldhmsubcALTV  39724  dmatALTval  39814  lincsumcl  39845  fdivval  39971
  Copyright terms: Public domain W3C validator