Theorem oveq12 7165

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537  (class class class)co 7156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  oveq12i  7168  oveq12d  7174  oveqan12d  7175  mptmpoopabovd  7779  suppofssd  7867  sprmpod  7890  oev2  8148  oa00  8185  omopthi  8284  ecopoveq  8398  ecopovtrn  8400  isfsupp  8837  cantnffval  9126  fpwwe2  10065  halfnq  10398  distrlem5pr  10449  addcmpblnr  10491  ltsrpr  10499  mulgt0sr  10527  add20  11152  msqge0  11161  recextlem2  11271  cru  11630  zaddcl  12023  qaddcl  12365  qmulcl  12367  xaddval  12617  xmulval  12619  xnn0xadd0  12641  xadddilem  12688  fzopth  12945  modval  13240  1exp  13459  m1expeven  13477  nn0opthi  13631  faclbnd  13651  faclbnd3  13653  bcn0  13671  ccatopth  14078  ccatopth2  14079  repswccat  14148  reval  14465  absval  14597  clim  14851  rlim  14852  fsumparts  15161  cpnnen  15582  dvds2add  15643  dvds2sub  15644  opoe  15712  omoe  15713  opeo  15714  omeo  15715  gcddvds  15852  gcdcl  15855  gcdeq0  15865  gcdneg  15870  gcdaddmlem  15872  gcdabs  15877  bezoutlem3  15889  bezout  15891  gcddiv  15899  eucalgval2  15925  lcmabs  15949  rpmul  16003  divgcdcoprmex  16010  isprm5  16051  prmexpb  16062  rpexp  16064  nn0gcdsq  16092  pcqmul  16190  prmreclem3  16254  mul4sq  16290  vdwapval  16309  f1ocpbl  16798  homfval  16962  comfval  16970  issect  17023  isfull  17180  isfth  17184  natfval  17216  catchom  17359  catcco  17361  funcsetcestrclem5  17409  plusfval  17859  0subm  17982  cycsubm  18345  cyccom  18346  isgim  18402  subgga  18430  cayleylem1  18540  lsmsubm  18778  subgdisjb  18819  pj1fval  18820  odadd1  18968  qusabl  18985  cygablOLD  19011  dprdsubg  19146  ringadd2  19325  dfrhm2  19469  isrhm  19473  isrim0  19475  scafval  19653  rmodislmodlem  19701  rmodislmod  19702  lss1d  19735  islmhm  19799  islmim  19834  mplval  20208  mplcoe5lem  20248  opsrval  20255  evlval  20308  mpfind  20320  selvffval  20329  mhpfval  20332  znfld  20707  cygznlem3  20716  cnmsgnsubg  20721  psgnghm  20724  ipeq0  20782  ipfval  20793  dsmmval  20878  dsmmacl  20885  mat1dimcrng  21086  dmatval  21101  dmatmulcl  21109  scmatval  21113  scmataddcl  21125  scmatsubcl  21126  scmatmulcl  21127  mavmul0g  21162  marrepfval  21169  marrepeval  21172  marepvfval  21174  marepveval  21177  submafval  21188  submaeval  21191  mdetfval  21195  madugsum  21252  minmar1fval  21255  minmar1eval  21258  symgmatr01  21263  gsummatr01lem3  21266  gsummatr01lem4  21267  gsummatr01  21268  cpmatacl  21324  mat2pmatfval  21331  mat2pmatvalel  21333  mat2pmatmul  21339  cpm2mfval  21357  cpm2mvalel  21359  m2cpminvid  21361  m2cpminvid2  21363  decpmate  21374  pmatcollpw1  21384  monmatcollpw  21387  pmatcollpwlem  21388  pmatcollpw  21389  pmatcollpwscmatlem2  21398  pm2mpval  21403  pm2mpf1  21407  mp2pm2mplem3  21416  mp2pm2mplem4  21417  chpmatfval  21438  tx2ndc  22259  cnmpt2t  22281  cnmpt22f  22283  hmeofval  22366  qustgplem  22729  stdbdmetval  23124  nmofval  23323  nghmfval  23331  isnmhm  23355  xrsxmet  23417  isphtpy  23585  isphtpc  23598  pcorevlem  23630  cphnm  23797  tcphnmval  23832  ipcau2  23837  tcphcphlem1  23838  tcphcphlem2  23839  tcphcph  23840  bcthlem1  23927  bcth  23932  dyadmax  24199  volcn  24207  vitalilem1  24209  vitalilem2  24210  vitalilem3  24211  vitali  24214  i1fmullem  24295  itg1addlem4  24300  dvlip  24590  ftc1a  24634  mdegfval  24656  r1pval  24750  coeaddlem  24839  quotval  24881  elqaalem2  24909  taylfval  24947  cxpcn3  25329  resqrtcn  25330  sqrtcn  25331  abscxpbnd  25334  angval  25379  chordthmlem  25410  dcubic  25424  lgsdchr  25931  mul2sq  25995  ostthlem2  26204  tglngval  26337  islnopp  26525  ishpg  26545  finsumvtxdg2size  27332  wspthsn  27626  wwlksnon  27629  wspthsnon  27630  iswspthsnon  27634  2clwwlk  28126  numclwlk1lem2  28149  numclwwlkovh0  28151  hmoval  28587  htth  28695  normval  28901  hlimi  28965  hsn0elch  29025  ocsh  29060  shscli  29094  shs00i  29227  chj00i  29264  riesz4i  29840  stm1addi  30022  stm1add3i  30024  superpos  30131  prmidlc  30964  brfinext  31043  submateq  31074  metidv  31132  rmulccn  31171  pl1cn  31198  sibfof  31598  cxpcncf1  31866  subfacval2  32434  txsconnlem  32487  iscvm  32506  prv  32675  bj-bary1  34596  ismblfin  34948  itg2addnclem3  34960  itg2addnc  34961  ftc1anclem3  34984  ftc1anc  34990  bfp  35117  rngo2  35200  rngohomco  35267  rngoisoval  35270  rngoisocnv  35274  crngohomfo  35299  keridl  35325  ispridlc  35363  snatpsubN  36901  cdlemn11pre  38361  dihord2pre  38376  baerlem3lem1  38858  nn0rppwr  39231  mendval  39832  mendplusg  39835  mulvval  40849  climf  41952  climf2  41996  cxpcncf2  42232  smflimlem3  43098  fzoopth  43576  fmtnofac2lem  43779  prmdvdsfmtnof1lem2  43796  opoeALTV  43897  opeoALTV  43898  rnghmval  44211  isrngisom  44216  rhmval  44239  rngchomALTV  44305  funcrngcsetcALT  44319  funcringcsetcALTV2lem5  44360  ringchomALTV  44368  funcringcsetclem5ALTV  44383  srhmsubclem3  44395  srhmsubc  44396  fldhmsubc  44404  srhmsubcALTVlem2  44413  srhmsubcALTV  44414  fldhmsubcALTV  44422  dmatALTval  44504  lincsumcl  44535  fdivval  44648