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

Theorem oveq12 5867
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 5865 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 5866 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2335 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623  (class class class)co 5858
This theorem is referenced by:  oveq12i  5870  oveq12d  5876  oveqan12d  5877  oev2  6522  oa00  6557  omopthi  6655  ecopoveq  6759  ecopovtrn  6761  th3qlem1  6764  th3qlem2  6765  cantnffval  7364  fpwwe2  8265  halfnq  8600  distrlem5pr  8651  addcmpblnr  8694  addsrpr  8697  mulsrpr  8698  ltsrpr  8699  mulgt0sr  8727  add20  9286  msqge0  9295  recextlem2  9399  cru  9738  zaddcl  10059  qaddcl  10332  qmulcl  10334  xaddval  10550  xmulval  10552  xadddilem  10614  fzopth  10828  modval  10975  1exp  11131  nn0opthi  11285  faclbnd  11303  faclbnd3  11305  bcn0  11323  ccatopth  11462  ccatopth2  11463  reval  11591  absval  11723  clim  11968  rlim  11969  fsumparts  12264  cpnnen  12507  dvds2add  12560  dvds2sub  12561  gcddvds  12694  gcdcl  12696  gcdeq0  12700  gcdneg  12705  gcdaddmlem  12707  gcdabs  12712  bezoutlem3  12719  bezout  12721  gcddiv  12728  eucalgval2  12751  isprm5  12791  prmexpb  12796  rpexp  12799  rpmul  12802  nn0gcdsq  12823  opoe  12864  omoe  12865  opeo  12866  omeo  12867  pcqmul  12906  prmreclem3  12965  mul4sq  13001  vdwapval  13020  f1ocpbl  13427  homfval  13595  comfval  13603  issect  13656  isfull  13784  isfth  13788  natfval  13820  catchom  13931  catcco  13933  plusfval  14380  isgim  14726  subgga  14754  cayleylem1  14787  lsmsubm  14964  subgdisjb  15002  pj1fval  15003  odadd1  15140  divsabl  15157  cygabl  15177  dprdsubg  15259  dfrhm2  15498  isrhm  15501  scafval  15646  lss1d  15720  islmhm  15784  islmim  15815  mplval  16173  opsrval  16216  znfld  16514  cygznlem3  16523  ipeq0  16542  ipfval  16553  tx2ndc  17345  cnmpt2t  17367  cnmpt22f  17369  hmeofval  17449  divstgplem  17803  stdbdmetval  18060  nmofval  18223  nghmfval  18231  isnmhm  18255  xrsxmet  18315  isphtpy  18479  isphtpc  18492  pcorevlem  18524  cphnm  18629  tchnmval  18660  ipcau2  18664  tchcphlem1  18665  tchcphlem2  18666  tchcph  18667  bcthlem1  18746  bcth  18751  dyadmax  18953  volcn  18961  vitalilem1  18963  vitalilem2  18964  vitalilem3  18965  vitali  18968  i1fmullem  19049  itg1addlem4  19054  dvlip  19340  ftc1a  19384  evlval  19408  mpfind  19428  mdegfval  19448  r1pval  19542  coeaddlem  19630  quotval  19672  elqaalem2  19700  taylfval  19738  cxpcn3  20088  resqrcn  20089  sqrcn  20090  abscxpbnd  20093  angval  20099  chordthmlem  20129  dcubic  20142  lgsdchr  20587  mul2sq  20604  ostthlem2  20777  ablosn  21014  rngo2  21055  hmoval  21388  htth  21498  normval  21703  hlimi  21767  hsn0elch  21827  ocsh  21862  shscli  21896  shs00i  22029  chj00i  22066  riesz4i  22643  stm1addi  22825  stm1add3i  22827  superpos  22934  rmulccn  23301  subfacval2  23718  txsconlem  23771  iscvm  23790  ghomgrpilem2  23993  ghomsn  23995  fprodsub  25379  hmeogrp  25537  idsubfun  25858  islimcat  25876  sgplpte21  26132  sgplpte22  26138  isray2  26153  isside1  26165  bosser  26167  bfp  26548  rngohomco  26605  rngoisoval  26608  rngoisocnv  26612  crngohomfo  26631  keridl  26657  ispridlc  26695  dsmmval  27200  dsmmacl  27207  cnmsgnsubg  27434  psgnghm  27437  mdetfval  27487  mendval  27491  mendplusg  27494  mulvval  27673  stoweidlem13  27762  snatpsubN  29939  cdlemn11pre  31400  dihord2pre  31415  baerlem3lem1  31897
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator