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

Theorem oveq12 6291
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 6289 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 6290 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2528 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379  (class class class)co 6282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285
This theorem is referenced by:  oveq12i  6294  oveq12d  6300  oveqan12d  6301  sprmpt2d  6949  oev2  7170  oa00  7205  omopthi  7303  ecopoveq  7409  ecopovtrn  7411  isfsupp  7829  cantnffval  8076  fpwwe2  9017  halfnq  9350  distrlem5pr  9401  addcmpblnr  9442  ltsrpr  9450  mulgt0sr  9478  add20  10060  msqge0  10070  recextlem2  10176  cru  10524  zaddcl  10899  qaddcl  11194  qmulcl  11196  xaddval  11418  xmulval  11420  xadddilem  11482  fzopth  11716  modval  11961  1exp  12157  nn0opthi  12312  faclbnd  12330  faclbnd3  12332  bcn0  12350  ccatopth  12652  ccatopth2  12653  repswccat  12714  reval  12896  absval  13028  clim  13273  rlim  13274  fsumparts  13576  cpnnen  13816  dvds2add  13869  dvds2sub  13870  gcddvds  14005  gcdcl  14007  gcdeq0  14011  gcdneg  14016  gcdaddmlem  14018  gcdabs  14023  bezoutlem3  14030  bezout  14032  gcddiv  14039  eucalgval2  14062  isprm5  14105  prmexpb  14110  rpexp  14113  rpmul  14116  nn0gcdsq  14137  opoe  14187  omoe  14188  opeo  14189  omeo  14190  pcqmul  14229  prmreclem3  14288  mul4sq  14324  vdwapval  14343  f1ocpbl  14773  homfval  14941  comfval  14949  issect  15002  isfull  15130  isfth  15134  natfval  15166  catchom  15277  catcco  15279  plusfval  15738  isgim  16102  subgga  16130  cayleylem1  16229  lsmsubm  16466  subgdisjb  16504  pj1fval  16505  odadd1  16644  divsabl  16661  cygabl  16681  dprdsubg  16858  dfrhm2  17147  isrhm  17151  isrim0  17153  scafval  17311  lss1d  17389  islmhm  17453  islmim  17488  mplval  17852  mplcoe5lem  17898  opsrval  17907  evlval  17961  mpfind  17973  znfld  18363  cygznlem3  18372  cnmsgnsubg  18377  psgnghm  18380  ipeq0  18437  ipfval  18448  dsmmval  18529  dsmmacl  18536  mat1dimcrng  18743  dmatval  18758  dmatmulcl  18766  scmatval  18770  scmataddcl  18782  scmatsubcl  18783  scmatmulcl  18784  mavmul0g  18819  marrepfval  18826  marrepeval  18829  marepvfval  18831  marepveval  18834  submafval  18845  submaeval  18848  mdetfval  18852  madugsum  18909  minmar1fval  18912  minmar1eval  18915  symgmatr01  18920  gsummatr01lem3  18923  gsummatr01lem4  18924  gsummatr01  18925  cpmatacl  18981  mat2pmatfval  18988  mat2pmatvalel  18990  mat2pmatmul  18996  cpm2mfval  19014  cpm2mvalel  19016  m2cpminvid  19018  m2cpminvid2  19020  decpmate  19031  pmatcollpw1  19041  monmatcollpw  19044  pmatcollpwlem  19045  pmatcollpw  19046  pmatcollpwscmatlem2  19055  pm2mpval  19060  pm2mpf1  19064  mp2pm2mplem3  19073  mp2pm2mplem4  19074  chpmatfval  19095  tx2ndc  19884  cnmpt2t  19906  cnmpt22f  19908  hmeofval  19991  divstgplem  20351  stdbdmetval  20749  nmofval  20953  nghmfval  20961  isnmhm  20985  xrsxmet  21046  isphtpy  21213  isphtpc  21226  pcorevlem  21258  cphnm  21372  tchnmval  21404  ipcau2  21409  tchcphlem1  21410  tchcphlem2  21411  tchcph  21412  bcthlem1  21495  bcth  21500  dyadmax  21739  volcn  21747  vitalilem1  21749  vitalilem2  21750  vitalilem3  21751  vitali  21754  i1fmullem  21833  itg1addlem4  21838  dvlip  22126  ftc1a  22170  mdegfval  22192  r1pval  22289  coeaddlem  22377  quotval  22419  elqaalem2  22447  taylfval  22485  cxpcn3  22847  resqrtcn  22848  sqrtcn  22849  abscxpbnd  22852  angval  22858  chordthmlem  22888  dcubic  22902  lgsdchr  23348  mul2sq  23365  ostthlem2  23538  tglngval  23663  wlkon  24206  wlkonprop  24208  trls  24211  trlon  24215  trlonprop  24217  pths  24241  spths  24242  pthon  24250  pthonprop  24252  spthon  24257  spthonprp  24260  isconngra  24345  isconngra1  24346  wwlkn  24355  clwlk  24426  clwlkcompim  24437  clwwlkn  24440  clwwlknprop  24445  is2wlkonot  24536  is2spthonot  24537  2wlkonot  24538  2spthonot  24539  2wlksot  24540  2spthsot  24541  2wlkonot3v  24548  2spthonot3v  24549  isrgra  24599  ablosn  25022  rngo2  25063  hmoval  25398  htth  25508  normval  25714  hlimi  25778  hsn0elch  25839  ocsh  25874  shscli  25908  shs00i  26041  chj00i  26078  riesz4i  26655  stm1addi  26837  stm1add3i  26839  superpos  26946  metidv  27504  rmulccn  27543  pl1cn  27570  sibfof  27919  subfacval2  28268  m1expevenALT  28300  txsconlem  28322  iscvm  28341  ghomgrpilem2  28498  ghomsn  28500  ismblfin  29630  itg2addnclem3  29643  itg2addnc  29644  ftc1anclem3  29667  ftc1anc  29673  bfp  29921  rngohomco  29978  rngoisoval  29981  rngoisocnv  29985  crngohomfo  30004  keridl  30030  ispridlc  30068  mendval  30737  mendplusg  30740  lcmabs  30811  mulvval  30955  climf  31164  fzoopth  31809  dmatALTval  32074  lincsumcl  32105  bj-bary1  33753  snatpsubN  34546  cdlemn11pre  36007  dihord2pre  36022  baerlem3lem1  36504
  Copyright terms: Public domain W3C validator