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

Theorem oveq12 6049
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 6047 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 6048 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2456 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649  (class class class)co 6040
This theorem is referenced by:  oveq12i  6052  oveq12d  6058  oveqan12d  6059  sprmpt2  6435  oev2  6726  oa00  6761  omopthi  6859  ecopoveq  6964  ecopovtrn  6966  th3qlem1  6969  th3qlem2  6970  cantnffval  7574  fpwwe2  8474  halfnq  8809  distrlem5pr  8860  addcmpblnr  8903  addsrpr  8906  mulsrpr  8907  ltsrpr  8908  mulgt0sr  8936  add20  9496  msqge0  9505  recextlem2  9609  cru  9948  zaddcl  10273  qaddcl  10546  qmulcl  10548  xaddval  10765  xmulval  10767  xadddilem  10829  fzopth  11045  modval  11207  1exp  11364  nn0opthi  11518  faclbnd  11536  faclbnd3  11538  bcn0  11556  ccatopth  11731  ccatopth2  11732  reval  11866  absval  11998  clim  12243  rlim  12244  fsumparts  12540  cpnnen  12783  dvds2add  12836  dvds2sub  12837  gcddvds  12970  gcdcl  12972  gcdeq0  12976  gcdneg  12981  gcdaddmlem  12983  gcdabs  12988  bezoutlem3  12995  bezout  12997  gcddiv  13004  eucalgval2  13027  isprm5  13067  prmexpb  13072  rpexp  13075  rpmul  13078  nn0gcdsq  13099  opoe  13140  omoe  13141  opeo  13142  omeo  13143  pcqmul  13182  prmreclem3  13241  mul4sq  13277  vdwapval  13296  f1ocpbl  13705  homfval  13873  comfval  13881  issect  13934  isfull  14062  isfth  14066  natfval  14098  catchom  14209  catcco  14211  plusfval  14658  isgim  15004  subgga  15032  cayleylem1  15065  lsmsubm  15242  subgdisjb  15280  pj1fval  15281  odadd1  15418  divsabl  15435  cygabl  15455  dprdsubg  15537  dfrhm2  15776  isrhm  15779  scafval  15924  lss1d  15994  islmhm  16058  islmim  16089  mplval  16447  opsrval  16490  znfld  16796  cygznlem3  16805  ipeq0  16824  ipfval  16835  tx2ndc  17636  cnmpt2t  17658  cnmpt22f  17660  hmeofval  17743  divstgplem  18103  stdbdmetval  18497  nmofval  18701  nghmfval  18709  isnmhm  18733  xrsxmet  18793  isphtpy  18959  isphtpc  18972  pcorevlem  19004  cphnm  19109  tchnmval  19140  ipcau2  19144  tchcphlem1  19145  tchcphlem2  19146  tchcph  19147  bcthlem1  19230  bcth  19235  dyadmax  19443  volcn  19451  vitalilem1  19453  vitalilem2  19454  vitalilem3  19455  vitali  19458  i1fmullem  19539  itg1addlem4  19544  dvlip  19830  ftc1a  19874  evlval  19898  mpfind  19918  mdegfval  19938  r1pval  20032  coeaddlem  20120  quotval  20162  elqaalem2  20190  taylfval  20228  cxpcn3  20585  resqrcn  20586  sqrcn  20587  abscxpbnd  20590  angval  20596  chordthmlem  20626  dcubic  20639  lgsdchr  21085  mul2sq  21102  ostthlem2  21275  wlkon  21483  wlkonprop  21485  trls  21489  trlon  21493  trlonprop  21495  pths  21519  spths  21520  pthon  21528  pthonprop  21530  spthon  21535  spthonprp  21538  isconngra  21612  isconngra1  21613  ablosn  21888  rngo2  21929  hmoval  22264  htth  22374  normval  22579  hlimi  22643  hsn0elch  22703  ocsh  22738  shscli  22772  shs00i  22905  chj00i  22942  riesz4i  23519  stm1addi  23701  stm1add3i  23703  superpos  23810  metidv  24240  rmulccn  24267  sibfof  24607  subfacval2  24826  m1expevenALT  24858  txsconlem  24880  iscvm  24899  ghomgrpilem2  25050  ghomsn  25052  ismblfin  26146  itg2addnclem3  26157  itg2addnc  26158  bfp  26423  rngohomco  26480  rngoisoval  26483  rngoisocnv  26487  crngohomfo  26506  keridl  26532  ispridlc  26570  dsmmval  27068  dsmmacl  27075  cnmsgnsubg  27302  psgnghm  27305  mdetfval  27355  mendval  27359  mendplusg  27362  mulvval  27540  swrdccat3b  28031  is2wlkonot  28060  is2spthonot  28061  2wlkonot  28062  2spthonot  28063  2wlksot  28064  2spthsot  28065  2wlkonot3v  28072  2spthonot3v  28073  snatpsubN  30232  cdlemn11pre  31693  dihord2pre  31708  baerlem3lem1  32190
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator