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

Theorem oveq12 6699
Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
Assertion
Ref Expression
oveq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 6697 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2 oveq2 6698 . 2 (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
31, 2sylan9eq 2705 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  (class class class)co 6690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  oveq12i  6702  oveq12d  6708  oveqan12d  6709  mptmpt2opabovd  7294  sprmpt2d  7395  oev2  7648  oa00  7684  omopthi  7782  ecopoveq  7891  ecopovtrn  7893  isfsupp  8320  cantnffval  8598  fpwwe2  9503  halfnq  9836  distrlem5pr  9887  addcmpblnr  9928  ltsrpr  9936  mulgt0sr  9964  add20  10578  msqge0  10587  recextlem2  10696  cru  11050  zaddcl  11455  qaddcl  11842  qmulcl  11844  xaddval  12092  xmulval  12094  xnn0xadd0  12115  xadddilem  12162  fzopth  12416  modval  12710  1exp  12929  m1expeven  12947  nn0opthi  13097  faclbnd  13117  faclbnd3  13119  bcn0  13137  ccatopth  13516  ccatopth2  13517  repswccat  13578  reval  13890  absval  14022  clim  14269  rlim  14270  fsumparts  14582  cpnnen  15002  dvds2add  15062  dvds2sub  15063  opoe  15134  omoe  15135  opeo  15136  omeo  15137  gcddvds  15272  gcdcl  15275  gcdeq0  15285  gcdneg  15290  gcdaddmlem  15292  gcdabs  15297  bezoutlem3  15305  bezout  15307  gcddiv  15315  eucalgval2  15341  lcmabs  15365  rpmul  15420  divgcdcoprmex  15427  isprm5  15466  prmexpb  15477  rpexp  15479  nn0gcdsq  15507  pcqmul  15605  prmreclem3  15669  mul4sq  15705  vdwapval  15724  f1ocpbl  16232  homfval  16399  comfval  16407  issect  16460  isfull  16617  isfth  16621  natfval  16653  catchom  16796  catcco  16798  funcsetcestrclem5  16846  plusfval  17295  isgim  17751  subgga  17779  cayleylem1  17878  lsmsubm  18114  subgdisjb  18152  pj1fval  18153  odadd1  18297  qusabl  18314  cygabl  18338  dprdsubg  18469  ringadd2  18621  dfrhm2  18765  isrhm  18769  isrim0  18771  scafval  18930  rmodislmodlem  18978  rmodislmod  18979  lss1d  19011  islmhm  19075  islmim  19110  mplval  19476  mplcoe5lem  19515  opsrval  19522  evlval  19572  mpfind  19584  znfld  19957  cygznlem3  19966  cnmsgnsubg  19971  psgnghm  19974  ipeq0  20031  ipfval  20042  dsmmval  20126  dsmmacl  20133  mat1dimcrng  20331  dmatval  20346  dmatmulcl  20354  scmatval  20358  scmataddcl  20370  scmatsubcl  20371  scmatmulcl  20372  mavmul0g  20407  marrepfval  20414  marrepeval  20417  marepvfval  20419  marepveval  20422  submafval  20433  submaeval  20436  mdetfval  20440  madugsum  20497  minmar1fval  20500  minmar1eval  20503  symgmatr01  20508  gsummatr01lem3  20511  gsummatr01lem4  20512  gsummatr01  20513  cpmatacl  20569  mat2pmatfval  20576  mat2pmatvalel  20578  mat2pmatmul  20584  cpm2mfval  20602  cpm2mvalel  20604  m2cpminvid  20606  m2cpminvid2  20608  decpmate  20619  pmatcollpw1  20629  monmatcollpw  20632  pmatcollpwlem  20633  pmatcollpw  20634  pmatcollpwscmatlem2  20643  pm2mpval  20648  pm2mpf1  20652  mp2pm2mplem3  20661  mp2pm2mplem4  20662  chpmatfval  20683  tx2ndc  21502  cnmpt2t  21524  cnmpt22f  21526  hmeofval  21609  qustgplem  21971  stdbdmetval  22366  nmofval  22565  nghmfval  22573  isnmhm  22597  xrsxmet  22659  isphtpy  22827  isphtpc  22840  pcorevlem  22872  cphnm  23039  tchnmval  23074  ipcau2  23079  tchcphlem1  23080  tchcphlem2  23081  tchcph  23082  bcthlem1  23167  bcth  23172  dyadmax  23412  volcn  23420  vitalilem1  23422  vitalilem2  23423  vitalilem3  23424  vitali  23427  i1fmullem  23506  itg1addlem4  23511  dvlip  23801  ftc1a  23845  mdegfval  23867  r1pval  23961  coeaddlem  24050  quotval  24092  elqaalem2  24120  taylfval  24158  cxpcn3  24534  resqrtcn  24535  sqrtcn  24536  abscxpbnd  24539  angval  24576  chordthmlem  24604  dcubic  24618  lgsdchr  25125  mul2sq  25189  ostthlem2  25362  tglngval  25491  islnopp  25676  ishpg  25696  finsumvtxdg2size  26502  wspthsn  26797  wwlksnon  26800  wspthsnon  26801  iswspthsnon  26806  iswspthsnonOLD  26807  2clwwlk  27335  numclwwlkovh0  27352  hmoval  27793  htth  27903  normval  28109  hlimi  28173  hsn0elch  28233  ocsh  28270  shscli  28304  shs00i  28437  chj00i  28474  riesz4i  29050  stm1addi  29232  stm1add3i  29234  superpos  29341  submateq  30003  metidv  30063  rmulccn  30102  pl1cn  30129  sibfof  30530  cxpcncf1  30801  subfacval2  31295  txsconnlem  31348  iscvm  31367  bj-bary1  33292  ismblfin  33580  itg2addnclem3  33593  itg2addnc  33594  ftc1anclem3  33617  ftc1anc  33623  bfp  33753  rngo2  33836  rngohomco  33903  rngoisoval  33906  rngoisocnv  33910  crngohomfo  33935  keridl  33961  ispridlc  33999  snatpsubN  35354  cdlemn11pre  36816  dihord2pre  36831  baerlem3lem1  37313  mendval  38070  mendplusg  38073  mulvval  38989  climf  40172  climf2  40216  cxpcncf2  40431  smflimlem3  41302  fzoopth  41662  fmtnofac2lem  41805  prmdvdsfmtnof1lem2  41822  opoeALTV  41919  opeoALTV  41920  rnghmval  42216  isrngisom  42221  rhmval  42244  rngchomALTV  42310  funcrngcsetcALT  42324  funcringcsetcALTV2lem5  42365  ringchomALTV  42373  funcringcsetclem5ALTV  42388  srhmsubclem3  42400  srhmsubc  42401  fldhmsubc  42409  srhmsubcALTVlem2  42418  srhmsubcALTV  42419  fldhmsubcALTV  42427  dmatALTval  42514  lincsumcl  42545  fdivval  42658
  Copyright terms: Public domain W3C validator