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

Theorem oveq12 6290
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 6288 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 6289 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2504 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1383  (class class class)co 6281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284
This theorem is referenced by:  oveq12i  6293  oveq12d  6299  oveqan12d  6300  sprmpt2d  6954  oev2  7175  oa00  7210  omopthi  7308  ecopoveq  7414  ecopovtrn  7416  isfsupp  7835  cantnffval  8083  fpwwe2  9024  halfnq  9357  distrlem5pr  9408  addcmpblnr  9449  ltsrpr  9457  mulgt0sr  9485  add20  10071  msqge0  10081  recextlem2  10187  cru  10535  zaddcl  10911  qaddcl  11209  qmulcl  11211  xaddval  11433  xmulval  11435  xadddilem  11497  fzopth  11731  modval  11980  1exp  12177  nn0opthi  12332  faclbnd  12350  faclbnd3  12352  bcn0  12370  ccatopth  12677  ccatopth2  12678  repswccat  12739  reval  12921  absval  13053  clim  13299  rlim  13300  fsumparts  13602  cpnnen  13944  dvds2add  13997  dvds2sub  13998  gcddvds  14135  gcdcl  14137  gcdeq0  14141  gcdneg  14146  gcdaddmlem  14148  gcdabs  14153  bezoutlem3  14160  bezout  14162  gcddiv  14169  eucalgval2  14192  isprm5  14235  prmexpb  14240  rpexp  14243  rpmul  14246  nn0gcdsq  14267  opoe  14317  omoe  14318  opeo  14319  omeo  14320  pcqmul  14359  prmreclem3  14418  mul4sq  14454  vdwapval  14473  f1ocpbl  14904  homfval  15069  comfval  15077  issect  15130  isfull  15258  isfth  15262  natfval  15294  catchom  15405  catcco  15407  plusfval  15857  isgim  16289  subgga  16317  cayleylem1  16416  lsmsubm  16652  subgdisjb  16690  pj1fval  16691  odadd1  16833  qusabl  16850  cygabl  16872  dprdsubg  17050  dfrhm2  17345  isrhm  17349  isrim0  17351  scafval  17510  lss1d  17588  islmhm  17652  islmim  17687  mplval  18063  mplcoe5lem  18109  opsrval  18118  evlval  18172  mpfind  18184  znfld  18577  cygznlem3  18586  cnmsgnsubg  18591  psgnghm  18594  ipeq0  18651  ipfval  18662  dsmmval  18743  dsmmacl  18750  mat1dimcrng  18957  dmatval  18972  dmatmulcl  18980  scmatval  18984  scmataddcl  18996  scmatsubcl  18997  scmatmulcl  18998  mavmul0g  19033  marrepfval  19040  marrepeval  19043  marepvfval  19045  marepveval  19048  submafval  19059  submaeval  19062  mdetfval  19066  madugsum  19123  minmar1fval  19126  minmar1eval  19129  symgmatr01  19134  gsummatr01lem3  19137  gsummatr01lem4  19138  gsummatr01  19139  cpmatacl  19195  mat2pmatfval  19202  mat2pmatvalel  19204  mat2pmatmul  19210  cpm2mfval  19228  cpm2mvalel  19230  m2cpminvid  19232  m2cpminvid2  19234  decpmate  19245  pmatcollpw1  19255  monmatcollpw  19258  pmatcollpwlem  19259  pmatcollpw  19260  pmatcollpwscmatlem2  19269  pm2mpval  19274  pm2mpf1  19278  mp2pm2mplem3  19287  mp2pm2mplem4  19288  chpmatfval  19309  tx2ndc  20130  cnmpt2t  20152  cnmpt22f  20154  hmeofval  20237  qustgplem  20597  stdbdmetval  20995  nmofval  21199  nghmfval  21207  isnmhm  21231  xrsxmet  21292  isphtpy  21459  isphtpc  21472  pcorevlem  21504  cphnm  21618  tchnmval  21650  ipcau2  21655  tchcphlem1  21656  tchcphlem2  21657  tchcph  21658  bcthlem1  21741  bcth  21746  dyadmax  21985  volcn  21993  vitalilem1  21995  vitalilem2  21996  vitalilem3  21997  vitali  22000  i1fmullem  22079  itg1addlem4  22084  dvlip  22372  ftc1a  22416  mdegfval  22438  r1pval  22535  coeaddlem  22624  quotval  22666  elqaalem2  22694  taylfval  22732  cxpcn3  23100  resqrtcn  23101  sqrtcn  23102  abscxpbnd  23105  angval  23111  chordthmlem  23141  dcubic  23155  lgsdchr  23601  mul2sq  23618  ostthlem2  23791  tglngval  23916  ishpg  24106  wlkon  24511  wlkonprop  24513  trls  24516  trlon  24520  trlonprop  24522  pths  24546  spths  24547  pthon  24555  pthonprop  24557  spthon  24562  spthonprp  24565  isconngra  24650  isconngra1  24651  wwlkn  24660  clwlk  24731  clwlkcompim  24742  clwwlkn  24745  clwwlknprop  24750  is2wlkonot  24841  is2spthonot  24842  2wlkonot  24843  2spthonot  24844  2wlksot  24845  2spthsot  24846  2wlkonot3v  24853  2spthonot3v  24854  isrgra  24904  ablosn  25327  rngo2  25368  hmoval  25703  htth  25813  normval  26019  hlimi  26083  hsn0elch  26144  ocsh  26179  shscli  26213  shs00i  26346  chj00i  26383  riesz4i  26960  stm1addi  27142  stm1add3i  27144  superpos  27251  metidv  27849  rmulccn  27888  pl1cn  27915  sibfof  28260  subfacval2  28609  m1expevenALT  28641  txsconlem  28663  iscvm  28682  ghomgrpilem2  29004  ghomsn  29006  ismblfin  30031  itg2addnclem3  30044  itg2addnc  30045  ftc1anclem3  30068  ftc1anc  30074  bfp  30296  rngohomco  30353  rngoisoval  30356  rngoisocnv  30360  crngohomfo  30379  keridl  30405  ispridlc  30443  mendval  31108  mendplusg  31111  lcmabs  31187  mulvval  31331  climf  31582  cxpcncf2  31657  fzoopth  32294  rnghmval  32532  isrngisom  32537  rhmval  32552  funcsetcestrclem5  32631  rngchomOLD  32668  funcrngcsetcALT  32682  funcringcsetcOLD2lem5  32720  ringchomOLD  32728  funcringcsetclem5OLD  32743  srhmsubclem3  32751  srhmsubc  32752  fldhmsubc  32760  srhmsubcOLDlem3  32770  srhmsubcOLD  32771  fldhmsubcOLD  32779  dmatALTval  32871  lincsumcl  32902  bj-bary1  34556  snatpsubN  35349  cdlemn11pre  36812  dihord2pre  36827  baerlem3lem1  37309
  Copyright terms: Public domain W3C validator