Theorem oveq12 7025

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522  (class class class)co 7016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-iota 6189  df-fv 6233  df-ov 7019

This theorem is referenced by:  oveq12i  7028  oveq12d  7034  oveqan12d  7035  mptmpoopabovd  7635  suppofssd  7718  sprmpod  7741  oev2  7999  oa00  8035  omopthi  8134  ecopoveq  8248  ecopovtrn  8250  isfsupp  8683  cantnffval  8972  fpwwe2  9911  halfnq  10244  distrlem5pr  10295  addcmpblnr  10337  ltsrpr  10345  mulgt0sr  10373  add20  11000  msqge0  11009  recextlem2  11119  cru  11478  zaddcl  11871  qaddcl  12214  qmulcl  12216  xaddval  12466  xmulval  12468  xnn0xadd0  12490  xadddilem  12537  fzopth  12794  modval  13089  1exp  13308  m1expeven  13326  nn0opthi  13480  faclbnd  13500  faclbnd3  13502  bcn0  13520  ccatopth  13914  ccatopth2  13915  repswccat  13984  reval  14299  absval  14431  clim  14685  rlim  14686  fsumparts  14994  cpnnen  15415  dvds2add  15476  dvds2sub  15477  opoe  15545  omoe  15546  opeo  15547  omeo  15548  gcddvds  15685  gcdcl  15688  gcdeq0  15698  gcdneg  15703  gcdaddmlem  15705  gcdabs  15710  bezoutlem3  15718  bezout  15720  gcddiv  15728  eucalgval2  15754  lcmabs  15778  rpmul  15832  divgcdcoprmex  15839  isprm5  15880  prmexpb  15891  rpexp  15893  nn0gcdsq  15921  pcqmul  16019  prmreclem3  16083  mul4sq  16119  vdwapval  16138  f1ocpbl  16627  homfval  16791  comfval  16799  issect  16852  isfull  17009  isfth  17013  natfval  17045  catchom  17188  catcco  17190  funcsetcestrclem5  17238  plusfval  17687  isgim  18143  subgga  18171  cayleylem1  18271  lsmsubm  18508  subgdisjb  18546  pj1fval  18547  odadd1  18691  qusabl  18708  cygabl  18732  dprdsubg  18863  ringadd2  19015  dfrhm2  19159  isrhm  19163  isrim0  19165  scafval  19343  rmodislmodlem  19391  rmodislmod  19392  lss1d  19425  islmhm  19489  islmim  19524  mplval  19896  mplcoe5lem  19935  opsrval  19942  evlval  19991  mpfind  20003  selvffval  20012  mhpfval  20015  znfld  20389  cygznlem3  20398  cnmsgnsubg  20403  psgnghm  20406  ipeq0  20464  ipfval  20475  dsmmval  20560  dsmmacl  20567  mat1dimcrng  20770  dmatval  20785  dmatmulcl  20793  scmatval  20797  scmataddcl  20809  scmatsubcl  20810  scmatmulcl  20811  mavmul0g  20846  marrepfval  20853  marrepeval  20856  marepvfval  20858  marepveval  20861  submafval  20872  submaeval  20875  mdetfval  20879  madugsum  20936  minmar1fval  20939  minmar1eval  20942  symgmatr01  20947  gsummatr01lem3  20950  gsummatr01lem4  20951  gsummatr01  20952  cpmatacl  21008  mat2pmatfval  21015  mat2pmatvalel  21017  mat2pmatmul  21023  cpm2mfval  21041  cpm2mvalel  21043  m2cpminvid  21045  m2cpminvid2  21047  decpmate  21058  pmatcollpw1  21068  monmatcollpw  21071  pmatcollpwlem  21072  pmatcollpw  21073  pmatcollpwscmatlem2  21082  pm2mpval  21087  pm2mpf1  21091  mp2pm2mplem3  21100  mp2pm2mplem4  21101  chpmatfval  21122  tx2ndc  21943  cnmpt2t  21965  cnmpt22f  21967  hmeofval  22050  qustgplem  22412  stdbdmetval  22807  nmofval  23006  nghmfval  23014  isnmhm  23038  xrsxmet  23100  isphtpy  23268  isphtpc  23281  pcorevlem  23313  cphnm  23480  tcphnmval  23515  ipcau2  23520  tcphcphlem1  23521  tcphcphlem2  23522  tcphcph  23523  bcthlem1  23610  bcth  23615  dyadmax  23882  volcn  23890  vitalilem1  23892  vitalilem2  23893  vitalilem3  23894  vitali  23897  i1fmullem  23978  itg1addlem4  23983  dvlip  24273  ftc1a  24317  mdegfval  24339  r1pval  24433  coeaddlem  24522  quotval  24564  elqaalem2  24592  taylfval  24630  cxpcn3  25010  resqrtcn  25011  sqrtcn  25012  abscxpbnd  25015  angval  25060  chordthmlem  25091  dcubic  25105  lgsdchr  25613  mul2sq  25677  ostthlem2  25886  tglngval  26019  islnopp  26207  ishpg  26227  finsumvtxdg2size  27015  wspthsn  27313  wwlksnon  27316  wspthsnon  27317  iswspthsnon  27321  2clwwlk  27818  numclwlk1lem2  27841  numclwwlkovh0  27843  hmoval  28278  htth  28386  normval  28592  hlimi  28656  hsn0elch  28716  ocsh  28751  shscli  28785  shs00i  28918  chj00i  28955  riesz4i  29531  stm1addi  29713  stm1add3i  29715  superpos  29822  brfinext  30647  submateq  30689  metidv  30749  rmulccn  30788  pl1cn  30815  sibfof  31215  cxpcncf1  31483  subfacval2  32043  txsconnlem  32096  iscvm  32115  prv  32284  bj-bary1  34149  ismblfin  34483  itg2addnclem3  34495  itg2addnc  34496  ftc1anclem3  34519  ftc1anc  34525  bfp  34653  rngo2  34736  rngohomco  34803  rngoisoval  34806  rngoisocnv  34810  crngohomfo  34835  keridl  34861  ispridlc  34899  snatpsubN  36436  cdlemn11pre  37896  dihord2pre  37911  baerlem3lem1  38393  nn0rppwr  38723  mendval  39287  mendplusg  39290  mulvval  40358  climf  41464  climf2  41508  cxpcncf2  41744  smflimlem3  42611  fzoopth  43063  fmtnofac2lem  43232  prmdvdsfmtnof1lem2  43249  opoeALTV  43350  opeoALTV  43351  rnghmval  43660  isrngisom  43665  rhmval  43688  rngchomALTV  43754  funcrngcsetcALT  43768  funcringcsetcALTV2lem5  43809  ringchomALTV  43817  funcringcsetclem5ALTV  43832  srhmsubclem3  43844  srhmsubc  43845  fldhmsubc  43853  srhmsubcALTVlem2  43862  srhmsubcALTV  43863  fldhmsubcALTV  43871  dmatALTval  43955  lincsumcl  43986  fdivval  44100