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

Theorem oveq12 5883
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 5881 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 5882 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2348 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632  (class class class)co 5874
This theorem is referenced by:  oveq12i  5886  oveq12d  5892  oveqan12d  5893  oev2  6538  oa00  6573  omopthi  6671  ecopoveq  6775  ecopovtrn  6777  th3qlem1  6780  th3qlem2  6781  cantnffval  7380  fpwwe2  8281  halfnq  8616  distrlem5pr  8667  addcmpblnr  8710  addsrpr  8713  mulsrpr  8714  ltsrpr  8715  mulgt0sr  8743  add20  9302  msqge0  9311  recextlem2  9415  cru  9754  zaddcl  10075  qaddcl  10348  qmulcl  10350  xaddval  10566  xmulval  10568  xadddilem  10630  fzopth  10844  modval  10991  1exp  11147  nn0opthi  11301  faclbnd  11319  faclbnd3  11321  bcn0  11339  ccatopth  11478  ccatopth2  11479  reval  11607  absval  11739  clim  11984  rlim  11985  fsumparts  12280  cpnnen  12523  dvds2add  12576  dvds2sub  12577  gcddvds  12710  gcdcl  12712  gcdeq0  12716  gcdneg  12721  gcdaddmlem  12723  gcdabs  12728  bezoutlem3  12735  bezout  12737  gcddiv  12744  eucalgval2  12767  isprm5  12807  prmexpb  12812  rpexp  12815  rpmul  12818  nn0gcdsq  12839  opoe  12880  omoe  12881  opeo  12882  omeo  12883  pcqmul  12922  prmreclem3  12981  mul4sq  13017  vdwapval  13036  f1ocpbl  13443  homfval  13611  comfval  13619  issect  13672  isfull  13800  isfth  13804  natfval  13836  catchom  13947  catcco  13949  plusfval  14396  isgim  14742  subgga  14770  cayleylem1  14803  lsmsubm  14980  subgdisjb  15018  pj1fval  15019  odadd1  15156  divsabl  15173  cygabl  15193  dprdsubg  15275  dfrhm2  15514  isrhm  15517  scafval  15662  lss1d  15736  islmhm  15800  islmim  15831  mplval  16189  opsrval  16232  znfld  16530  cygznlem3  16539  ipeq0  16558  ipfval  16569  tx2ndc  17361  cnmpt2t  17383  cnmpt22f  17385  hmeofval  17465  divstgplem  17819  stdbdmetval  18076  nmofval  18239  nghmfval  18247  isnmhm  18271  xrsxmet  18331  isphtpy  18495  isphtpc  18508  pcorevlem  18540  cphnm  18645  tchnmval  18676  ipcau2  18680  tchcphlem1  18681  tchcphlem2  18682  tchcph  18683  bcthlem1  18762  bcth  18767  dyadmax  18969  volcn  18977  vitalilem1  18979  vitalilem2  18980  vitalilem3  18981  vitali  18984  i1fmullem  19065  itg1addlem4  19070  dvlip  19356  ftc1a  19400  evlval  19424  mpfind  19444  mdegfval  19464  r1pval  19558  coeaddlem  19646  quotval  19688  elqaalem2  19716  taylfval  19754  cxpcn3  20104  resqrcn  20105  sqrcn  20106  abscxpbnd  20109  angval  20115  chordthmlem  20145  dcubic  20158  lgsdchr  20603  mul2sq  20620  ostthlem2  20793  ablosn  21030  rngo2  21071  hmoval  21404  htth  21514  normval  21719  hlimi  21783  hsn0elch  21843  ocsh  21878  shscli  21912  shs00i  22045  chj00i  22082  riesz4i  22659  stm1addi  22841  stm1add3i  22843  superpos  22950  rmulccn  23316  subfacval2  23733  txsconlem  23786  iscvm  23805  ghomgrpilem2  24008  ghomsn  24010  itg2addnclem  25003  itg2addnc  25005  fprodsub  25482  hmeogrp  25640  idsubfun  25961  islimcat  25979  sgplpte21  26235  sgplpte22  26241  isray2  26256  isside1  26268  bosser  26270  bfp  26651  rngohomco  26708  rngoisoval  26711  rngoisocnv  26715  crngohomfo  26734  keridl  26760  ispridlc  26798  dsmmval  27303  dsmmacl  27310  cnmsgnsubg  27537  psgnghm  27540  mdetfval  27590  mendval  27594  mendplusg  27597  mulvval  27776  stoweidlem13  27865  sprmpt2  28207  iswlkon  28332  trls  28335  trlon  28339  istrlon  28340  trlonprop  28341  pths  28352  spths  28353  pthon  28361  snatpsubN  30561  cdlemn11pre  32022  dihord2pre  32037  baerlem3lem1  32519
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877
  Copyright terms: Public domain W3C validator