Theorem oveq12 7371

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  (class class class)co 7362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6450  df-fv 6502  df-ov 7365

This theorem is referenced by:  oveq12i  7374  oveq12d  7380  oveqan12d  7381  ovmpot  7523  mptmpoopabovd  8029  suppofssd  8148  sprmpod  8169  oev2  8453  oa00  8489  omopthi  8592  ecopoveq  8760  ecopovtrn  8762  isfsupp  9273  cantnffval  9579  ttrcltr  9632  fpwwe2lem4  10552  fpwwe2  10561  pwfseqlem4  10580  halfnq  10894  distrlem5pr  10945  addcmpblnr  10987  ltsrpr  10995  mulgt0sr  11023  add20  11657  msqge0  11666  recextlem2  11776  cru  12146  zaddcl  12562  qaddcl  12910  qmulcl  12912  xaddval  13170  xmulval  13172  xnn0xadd0  13194  xadddilem  13241  fzopth  13510  fzoopth  13712  modval  13825  1exp  14048  m1expeven  14066  nn0opthi  14227  faclbnd  14247  faclbnd3  14249  bcn0  14267  ccatopth  14673  ccatopth2  14674  repswccat  14743  reval  15063  absval  15195  clim  15451  rlim  15452  fsumparts  15764  cpnnen  16191  dvds2add  16254  dvds2sub  16255  opoe  16327  omoe  16328  opeo  16329  omeo  16330  gcddvds  16467  gcdcl  16470  gcdeq0  16481  gcdneg  16486  gcdaddmlem  16488  bezoutlem3  16505  bezout  16507  gcddiv  16515  nn0rppwr  16525  eucalgval2  16545  lcmabs  16569  rpmul  16623  divgcdcoprmex  16630  isprm5  16672  prmexpb  16684  rpexp  16687  nn0gcdsq  16717  pcqmul  16819  prmreclem3  16884  mul4sq  16920  vdwapval  16939  f1ocpbl  17484  homfval  17653  comfval  17661  issect  17715  isfull  17874  isfth  17878  natfval  17911  catchom  18065  catcco  18067  funcsetcestrclem5  18120  plusfval  18610  0subm  18780  cycsubm  19172  cyccom  19173  isgim  19232  subgga  19270  cayleylem1  19382  lsmsubm  19623  subgdisjb  19663  pj1fval  19664  odadd1  19818  qusabl  19835  imasabl  19846  dprdsubg  19996  rnghmval  20415  isrngim  20420  dfrhm2  20449  isrhm  20453  isrim0  20457  rhmval  20472  funcrngcsetcALT  20613  srhmsubclem3  20651  srhmsubc  20652  fldhmsubc  20757  scafval  20871  rmodislmodlem  20919  rmodislmod  20920  lss1d  20953  islmhm  21018  islmim  21053  pzriprnglem5  21479  pzriprnglem8  21482  znfld  21554  cygznlem3  21563  cnmsgnsubg  21571  psgnghm  21574  ipeq0  21632  ipfval  21643  dsmmval  21728  dsmmacl  21735  mplval  21981  mplcoe5lem  22031  opsrval  22038  evlval  22092  mpfind  22107  selvffval  22113  mhpfval  22118  mhpmulcl  22129  psdffval  22137  mat1dimcrng  22456  dmatval  22471  dmatmulcl  22479  scmatval  22483  scmataddcl  22495  scmatsubcl  22496  scmatmulcl  22497  mavmul0g  22532  marrepfval  22539  marrepeval  22542  marepvfval  22544  marepveval  22547  submafval  22558  submaeval  22561  mdetfval  22565  madugsum  22622  minmar1fval  22625  minmar1eval  22628  symgmatr01  22633  gsummatr01lem3  22636  gsummatr01lem4  22637  gsummatr01  22638  cpmatacl  22695  mat2pmatfval  22702  mat2pmatvalel  22704  mat2pmatmul  22710  cpm2mfval  22728  cpm2mvalel  22730  m2cpminvid  22732  m2cpminvid2  22734  decpmate  22745  pmatcollpw1  22755  monmatcollpw  22758  pmatcollpwlem  22759  pmatcollpw  22760  pmatcollpwscmatlem2  22769  pm2mpval  22774  pm2mpf1  22778  mp2pm2mplem3  22787  mp2pm2mplem4  22788  chpmatfval  22809  tx2ndc  23630  cnmpt2t  23652  cnmpt22f  23654  hmeofval  23737  qustgplem  24100  stdbdmetval  24493  nmofval  24693  nghmfval  24701  isnmhm  24725  xrsxmet  24789  divcn  24849  divccn  24854  iihalf1cn  24913  iihalf2cn  24915  icchmeo  24922  cnrehmeo  24934  isphtpy  24962  isphtpc  24975  reparphti  24978  pcorevlem  25007  cphnm  25174  tcphnmval  25210  ipcau2  25215  tcphcphlem1  25216  tcphcphlem2  25217  tcphcph  25218  bcthlem1  25305  bcth  25310  mulcncf  25427  dyadmax  25579  volcn  25587  vitalilem1  25589  vitalilem2  25590  vitalilem3  25591  vitali  25594  i1fmullem  25675  itg1addlem4  25680  dvlip  25974  ftc1a  26018  mdegfval  26041  r1pval  26137  coeaddlem  26228  plycn  26240  quotval  26273  elqaalem2  26301  taylfval  26339  psercn2  26405  cxpcn  26726  cxpcn3  26729  resqrtcn  26730  sqrtcn  26731  abscxpbnd  26734  angval  26782  chordthmlem  26813  dcubic  26827  efrlim  26950  lgsdchr  27336  mul2sq  27400  ostthlem2  27609  zaddscl  28404  zmulscld  28407  zseo  28432  z12addscl  28487  tglngval  28637  islnopp  28825  ishpg  28845  finsumvtxdg2size  29638  wspthsn  29935  wwlksnon  29938  wspthsnon  29939  iswspthsnon  29943  2clwwlk  30436  numclwlk1lem2  30459  numclwwlkovh0  30461  hmoval  30900  htth  31008  normval  31214  hlimi  31278  hsn0elch  31338  ocsh  31373  shscli  31407  shs00i  31540  chj00i  31577  riesz4i  32153  stm1addi  32335  stm1add3i  32337  superpos  32444  elrgspnlem2  33323  prmidlc  33527  idlsrgmulrval  33588  splyval  33722  brfinext  33816  finextfldext  33828  irngval  33849  minplyval  33869  submateq  33973  metidv  34056  rmulccn  34092  pl1cn  34119  sibfof  34504  cxpcncf1  34759  subfacval2  35389  txsconnlem  35442  cvxpconn  35444  cvxsconn  35445  iscvm  35461  prv  35630  mpomulnzcnf  36501  knoppcnlem10  36782  bj-bary1  37646  ismblfin  38000  itg2addnclem3  38012  itg2addnc  38013  ftc1anclem3  38034  ftc1anc  38040  bfp  38163  rngo2  38246  rngohomco  38313  rngoisoval  38316  rngoisocnv  38320  crngohomfo  38345  keridl  38371  ispridlc  38409  snatpsubN  40214  cdlemn11pre  41674  dihord2pre  41689  baerlem3lem1  42171  prjcrvfval  43082  mendval  43629  mendplusg  43632  omcl3g  43784  mulvval  44916  fprodcnlem  46051  climf  46074  climf2  46116  cxpcncf2  46349  smflimlem3  47223  fmtnofac2lem  48047  prmdvdsfmtnof1lem2  48064  opoeALTV  48175  opeoALTV  48176  rngchomALTV  48760  funcringcsetcALTV2lem5  48786  ringchomALTV  48794  funcringcsetclem5ALTV  48809  srhmsubcALTVlem2  48816  srhmsubcALTV  48817  fldhmsubcALTV  48825  dmatALTval  48892  lincsumcl  48923  fdivval  49031  catprslem  49501  catprsc  49504  catprsc2  49505  oppcendc  49509  thincmoALT  49920  functhinclem2  49936  fullthinc2  49942  setc1onsubc  50093  lmdfval  50140  cmdfval  50141