Theorem oveq12 7425

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 7423	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2		oveq2 7424	. 2 ⊢ (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
3	1, 2	sylan9eq 2817	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419

This theorem is used by:  oveq12i  7428  oveq12d  7434  oveqan12d  7435  ovmpot  7577  mptmpoopabovd  8084  suppofssd  8204  sprmpod  8225  oev2  8513  oa00  8549  omopthi  8652  ecopoveq  8821  ecopovtrn  8823  isfsupp  9338  cantnffval  9645  ttrcltr  9698  fpwwe2lem4  10644  fpwwe2  10653  pwfseqlem4  10672  halfnq  10986  distrlem5pr  11037  addcmpblnr  11079  ltsrpr  11087  mulgt0sr  11115  add20  11751  msqge0  11760  recextlem2  11870  cru  12235  zaddcl  12659  qaddcl  13015  qmulcl  13017  xaddval  13275  xmulval  13277  xnn0xadd0  13299  xadddilem  13346  fzopth  13616  fzoopth  13818  modval  13932  1exp  14155  m1expeven  14173  nn0opthi  14334  faclbnd  14354  faclbnd3  14356  bcn0  14374  ccatopth  14785  ccatopth2  14786  repswccat  14857  reval  15193  absval  15325  clim  15581  rlim  15582  fsumparts  15893  cpnnen  16319  dvds2add  16382  dvds2sub  16383  opoe  16455  omoe  16456  opeo  16457  omeo  16458  gcddvds  16595  gcdcl  16598  gcdeq0  16609  gcdneg  16614  gcdaddmlem  16616  bezoutlem3  16633  bezout  16635  gcddiv  16643  nn0rppwr  16653  eucalgval2  16673  lcmabs  16697  rpmul  16751  divgcdcoprmex  16758  isprm5  16800  prmexpb  16812  rpexp  16815  nn0gcdsq  16845  pcqmul  16947  prmreclem3  17012  mul4sq  17048  vdwapval  17067  f1ocpbl  17613  homfval  17782  comfval  17790  issect  17844  isfull  18003  isfth  18007  natfval  18040  catchom  18194  catcco  18196  funcsetcestrclem5  18249  plusfval  18739  0subm  18925  cycsubm  19329  cyccom  19330  isgim  19388  subgga  19426  cayleylem1  19538  lsmsubm  19779  subgdisjb  19819  pj1fval  19820  odadd1  19974  qusabl  19991  imasabl  20002  dprdsubg  20152  rnghmval  20580  isrngim  20585  dfrhm2  20614  rhmval0  20615  isrhm  20619  isrim0  20623  crngrhmfo  20636  rhmval  20648  funcrngcsetcALT  20802  srhmsubclem3  20840  srhmsubc  20841  fldhmsubc  20950  scafval  21064  rmodislmodlem  21112  rmodislmod  21113  lss1d  21146  islmhm  21210  islmim  21245  prmidlc  21535  pzriprnglem5  21697  pzriprnglem8  21700  znfld  21772  cygznlem3  21781  cnmsgnsubg  21789  psgnghm  21792  ipeq0  21850  ipfval  21861  dsmmval  21946  dsmmacl  21953  mplval  22202  mplcoe5lem  22254  opsrval  22261  evlval  22315  mpfind  22330  selvffval  22333  mhpfval  22365  mhpmulcl  22376  psdffval  22384  mat1dimcrng  22698  dmatval  22713  dmatmulcl  22721  scmatval  22725  scmataddcl  22737  scmatsubcl  22738  scmatmulcl  22739  mavmul0g  22774  marrepfval  22781  marrepeval  22784  marepvfval  22786  marepveval  22789  submafval  22800  submaeval  22803  mdetfval  22807  madugsum  22864  minmar1fval  22867  minmar1eval  22870  symgmatr01  22875  gsummatr01lem3  22878  gsummatr01lem4  22879  gsummatr01  22880  cpmatacl  22940  mat2pmatfval  22947  mat2pmatvalel  22949  mat2pmatmul  22955  cpm2mfval  22973  cpm2mvalel  22975  m2cpminvid  22977  m2cpminvid2  22979  decpmate  22990  pmatcollpw1  23000  monmatcollpw  23003  pmatcollpwlem  23004  pmatcollpw  23005  pmatcollpwscmatlem2  23014  pm2mpval  23019  pm2mpf1  23023  mp2pm2mplem3  23032  mp2pm2mplem4  23033  chpmatfval  23054  tx2ndc  23876  cnmpt2t  23898  cnmpt22f  23900  hmeofval  23983  qustgplem  24346  stdbdmetval  24739  nmofval  24939  nghmfval  24947  isnmhm  24971  xrsxmet  25035  divcn  25095  divccn  25100  iihalf1cn  25159  iihalf2cn  25161  icchmeo  25168  cnrehmeo  25180  isphtpy  25208  isphtpc  25221  reparphti  25224  pcorevlem  25253  cphnm  25420  tcphnmval  25456  ipcau2  25461  tcphcphlem1  25462  tcphcphlem2  25463  tcphcph  25464  bcthlem1  25551  bcth  25556  mulcncf  25673  dyadmax  25825  volcn  25833  vitalilem1  25835  vitalilem2  25836  vitalilem3  25837  vitali  25840  i1fmullem  25921  itg1addlem4  25926  dvlip  26220  ftc1a  26264  mdegfval  26287  r1pval  26383  coeaddlem  26474  plycn  26486  quotval  26521  elqaalem2  26549  taylfval  26590  psercn2  26654  cxpcn  26978  cxpcn3  26981  resqrtcn  26982  sqrtcn  26983  abscxpbnd  26986  angval  27034  chordthmlem  27065  dcubic  27079  efrlim  27202  lgsdchr  27587  mul2sq  27651  ostthlem2  27860  zaddscl  28655  zmulscld  28658  zseo  28683  z12addscl  28738  tglngval  28889  islnopp  29090  ishpg  29112  elplngid  29135  lnincplng  29137  plngcp  29139  plngrot  29143  nhpmirhp  29151  lnperpexs  29185  ragraghl  29221  tgaaddcpbllem2  29225  tgaaddcpbl2  29228  angmndaddeu1  29250  prlnghpg  29287  prlngmo  29295  finsumvtxdg2size  29994  wspthsn  30300  wwlksnon  30303  wspthsnon  30304  iswspthsnon  30308  2clwwlk  30811  numclwlk1lem2  30834  numclwwlkovh0  30836  hmoval  31275  htth  31383  normval  31589  hlimi  31653  hsn0elch  31713  ocsh  31748  shscli  31782  shs00i  31915  chj00i  31952  riesz4i  32528  stm1addi  32710  stm1add3i  32712  superpos  32819  elrgspnlem2  33668  drnglring  33887  idlsrgmulrval  33904  splyval  34054  brfinext  34147  finextfldext  34159  irngval  34180  minplyval  34200  submateq  34304  metidv  34387  rmulccn  34423  pl1cn  34450  sibfof  34836  cxpcncf1  35088  subfacval2  35751  txsconnlem  35804  cvxpconn  35806  cvxsconn  35807  iscvm  35823  prv  35992  mpomulnzcnf  36904  knoppcnlem10  37184  bj-bary1  38049  ismblfin  38395  itg2addnclem3  38407  itg2addnc  38408  ftc1anclem3  38429  ftc1anc  38435  bfp  38559  rngo2  38642  rngohomco  38709  rngoisoval  38712  rngoisocnv  38716  crngohomfo  38741  keridl  38767  ispridlc  38805  snatpsubN  40608  cdlemn11pre  42068  dihord2pre  42083  baerlem3lem1  42565  prjcrvfval  43462  mendval  44005  mendplusg  44008  omcl3g  44160  mulvval  45275  fprodcnlem  46414  climf  46437  climf2  46479  cxpcncf2  46712  smflimlem3  47586  fmtnofac2lem  48456  prmdvdsfmtnof1lem2  48473  opoeALTV  48584  opeoALTV  48585  rngchomALTV  49168  funcringcsetcALTV2lem5  49194  ringchomALTV  49202  funcringcsetclem5ALTV  49217  srhmsubcALTVlem2  49224  srhmsubcALTV  49225  fldhmsubcALTV  49233  dmatALTval  49315  lincsumcl  49346  fdivval  49454  catprslem  49921  catprsc  49924  catprsc2  49925  oppcendc  49929  thincmoALT  50340  functhinclem2  50356  fullthinc2  50362  setc1onsubc  50513  lmdfval  50560  cmdfval  50561  crosspdot0lem  50778