Theorem oveq12 7429

Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)

Assertion

Ref	Expression
oveq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveq12

Step	Hyp	Ref	Expression
1		oveq1 7427	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2		oveq2 7428	. 2 ⊢ (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
3	1, 2	sylan9eq 2815	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  (class class class)co 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  oveq12i  7432  oveq12d  7438  oveqan12d  7439  ovmpot  7581  mptmpoopabovd  8095  suppofssd  8220  sprmpod  8241  oev2  8531  oa00  8567  omopthi  8670  ecopoveq  8839  ecopovtrn  8841  isfsupp  9357  cantnffval  9664  ttrcltr  9717  fpwwe2lem4  10719  fpwwe2  10728  pwfseqlem4  10747  halfnq  11061  distrlem5pr  11112  addcmpblnr  11154  ltsrpr  11162  mulgt0sr  11190  add20  11828  msqge0  11837  recextlem2  11947  cru  12312  zaddcl  12736  qaddcl  13093  qmulcl  13095  xaddval  13353  xmulval  13355  xnn0xadd0  13377  xadddilem  13424  fzopth  13695  fzoopth  13897  modval  14011  1exp  14234  m1expeven  14252  nn0opthi  14414  faclbnd  14434  faclbnd3  14436  bcn0  14454  ccatopth  14865  ccatopth2  14866  repswccat  14937  reval  15273  absval  15405  clim  15661  rlim  15662  fsumparts  15973  cpnnen  16397  dvds2add  16460  dvds2sub  16461  opoe  16533  omoe  16534  opeo  16535  omeo  16536  gcddvds  16673  gcdcl  16676  gcdeq0  16689  gcdneg  16694  gcdaddmlem  16696  bezoutlem3  16714  bezout  16716  gcddiv  16724  nn0rppwr  16735  eucalgval2  16756  lcmabs  16780  rpmul  16834  divgcdcoprmex  16841  isprm5  16883  prmexpb  16895  rpexp  16898  nn0gcdsq  16928  pcqmul  17031  prmreclem3  17096  mul4sq  17132  vdwapval  17151  f1ocpbl  17697  homfval  17866  comfval  17874  issect  17928  isfull  18087  isfth  18091  natfval  18124  catchom  18278  catcco  18280  funcsetcestrclem5  18333  plusfval  18823  0subm  19013  cycsubm  19417  cyccom  19418  isgim  19476  subgga  19514  cayleylem1  19626  lsmsubm  19867  subgdisjb  19907  pj1fval  19908  odadd1  20062  qusabl  20079  imasabl  20090  dprdsubg  20240  rnghmval  20670  isrngim  20675  dfrhm2  20704  rhmval0  20705  isrhm  20709  isrim0  20713  crngrhmfo  20726  rhmval  20738  funcrngcsetcALT  20893  srhmsubclem3  20931  srhmsubc  20932  fldhmsubc  21042  scafval  21156  rmodislmodlem  21204  rmodislmod  21205  lss1d  21238  islmhm  21302  islmim  21337  prmidlc  21629  pzriprnglem5  21791  pzriprnglem8  21794  znfld  21866  cygznlem3  21875  cnmsgnsubg  21883  psgnghm  21886  ipeq0  21944  ipfval  21955  dsmmval  22040  dsmmacl  22047  mplval  22296  mplcoe5lem  22348  opsrval  22355  evlval  22409  mpfind  22424  selvffval  22427  mhpfval  22459  mhpmulcl  22470  psdffval  22478  mat1dimcrng  22792  dmatval  22807  dmatmulcl  22815  scmatval  22819  scmataddcl  22831  scmatsubcl  22832  scmatmulcl  22833  mavmul0g  22868  marrepfval  22875  marrepeval  22878  marepvfval  22880  marepveval  22883  submafval  22894  submaeval  22897  mdetfval  22901  madugsum  22958  minmar1fval  22961  minmar1eval  22964  symgmatr01  22969  gsummatr01lem3  22972  gsummatr01lem4  22973  gsummatr01  22974  cpmatacl  23034  mat2pmatfval  23041  mat2pmatvalel  23043  mat2pmatmul  23049  cpm2mfval  23067  cpm2mvalel  23069  m2cpminvid  23071  m2cpminvid2  23073  decpmate  23084  pmatcollpw1  23094  monmatcollpw  23097  pmatcollpwlem  23098  pmatcollpw  23099  pmatcollpwscmatlem2  23108  pm2mpval  23113  pm2mpf1  23117  mp2pm2mplem3  23126  mp2pm2mplem4  23127  chpmatfval  23148  tx2ndc  23970  cnmpt2t  23992  cnmpt22f  23994  hmeofval  24077  qustgplem  24440  stdbdmetval  24833  nmofval  25033  nghmfval  25041  isnmhm  25065  xrsxmet  25129  divcn  25189  divccn  25194  iihalf1cn  25253  iihalf2cn  25255  icchmeo  25262  cnrehmeo  25274  isphtpy  25302  isphtpc  25315  reparphti  25318  pcorevlem  25347  cphnm  25514  tcphnmval  25550  ipcau2  25555  tcphcphlem1  25556  tcphcphlem2  25557  tcphcph  25558  bcthlem1  25645  bcth  25650  mulcncf  25767  dyadmax  25919  volcn  25927  vitalilem1  25929  vitalilem2  25930  vitalilem3  25931  vitali  25934  i1fmullem  26015  itg1addlem4  26020  dvlip  26313  ftc1a  26357  mdegfval  26380  r1pval  26476  coeaddlem  26568  plycn  26580  quotval  26613  elqaalem2  26643  taylfval  26686  psercn2  26750  cxpcn  27073  cxpcn3  27076  resqrtcn  27077  sqrtcn  27078  abscxpbnd  27081  angval  27129  chordthmlem  27160  dcubic  27174  efrlim  27297  lgsdchr  27682  mul2sq  27746  ostthlem2  27955  zaddscl  28780  zmulscld  28783  zseo  28808  z12addscl  28863  tglngval  29014  islnopp  29215  ishpg  29237  elplngid  29260  lnincplng  29262  plngcp  29264  plngrot  29268  nhpmirhp  29276  lnperpexs  29310  ragraghl  29346  tgaaddcpbllem2  29350  tgaaddcpbl2  29353  angmgmaddeu1  29379  prlnghpg  29424  prlngmo  29432  finsumvtxdg2size  30131  wspthsn  30437  wwlksnon  30440  wspthsnon  30441  iswspthsnon  30445  2clwwlk  30948  numclwlk1lem2  30971  numclwwlkovh0  30973  hmoval  31412  htth  31520  normval  31726  hlimi  31790  hsn0elch  31850  ocsh  31885  shscli  31919  shs00i  32052  chj00i  32089  riesz4i  32665  stm1addi  32847  stm1add3i  32849  superpos  32956  elrgspnlem2  33804  drnglring  34024  idlsrgmulrval  34041  splyval  34191  brfinext  34284  finextfldext  34296  irngval  34317  minplyval  34337  submateq  34441  metidv  34524  rmulccn  34560  pl1cn  34587  sibfof  34972  cxpcncf1  35224  subfacval2  35952  txsconnlem  36005  cvxpconn  36007  cvxsconn  36008  iscvm  36024  prv  36193  mpomulnzcnf  37088  knoppcnlem10  37368  bj-bary1  38234  ismblfin  38580  itg2addnclem3  38592  itg2addnc  38593  ftc1anclem3  38614  ftc1anc  38620  bfp  38759  rngo2  38842  rngohomco  38909  rngoisoval  38912  rngoisocnv  38916  crngohomfo  38941  keridl  38967  ispridlc  39005  snatpsubN  40808  cdlemn11pre  42268  dihord2pre  42283  baerlem3lem1  42765  prjcrvfval  43668  mendval  44181  mendplusg  44184  omcl3g  44336  mulvval  45450  fprodcnlem  46611  climf  46634  climf2  46676  cxpcncf2  46909  smflimlem3  47783  fmtnofac2lem  48653  prmdvdsfmtnof1lem2  48670  opoeALTV  48781  opeoALTV  48782  rngchomALTV  49365  funcringcsetcALTV2lem5  49391  ringchomALTV  49399  funcringcsetclem5ALTV  49414  srhmsubcALTVlem2  49421  srhmsubcALTV  49422  fldhmsubcALTV  49430  dmatALTval  49512  lincsumcl  49543  fdivval  49651  catprslem  50118  catprsc  50121  catprsc2  50122  oppcendc  50126  thincmoALT  50537  functhinclem2  50553  fullthinc2  50559  setc1onsubc  50710  lmdfval  50757  cmdfval  50758  crosspdot0lem  50963