Theorem oveq12 7365

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  (class class class)co 7356

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  oveq12i  7368  oveq12d  7374  oveqan12d  7375  ovmpot  7517  mptmpoopabovd  8024  suppofssd  8143  sprmpod  8164  oev2  8448  oa00  8484  omopthi  8587  ecopoveq  8753  ecopovtrn  8755  isfsupp  9266  cantnffval  9570  ttrcltr  9623  fpwwe2lem4  10543  fpwwe2  10552  pwfseqlem4  10571  halfnq  10885  distrlem5pr  10936  addcmpblnr  10978  ltsrpr  10986  mulgt0sr  11014  add20  11647  msqge0  11656  recextlem2  11766  cru  12135  zaddcl  12529  qaddcl  12876  qmulcl  12878  xaddval  13136  xmulval  13138  xnn0xadd0  13160  xadddilem  13207  fzopth  13475  fzoopth  13676  modval  13789  1exp  14012  m1expeven  14030  nn0opthi  14191  faclbnd  14211  faclbnd3  14213  bcn0  14231  ccatopth  14637  ccatopth2  14638  repswccat  14707  reval  15027  absval  15159  clim  15415  rlim  15416  fsumparts  15727  cpnnen  16152  dvds2add  16215  dvds2sub  16216  opoe  16288  omoe  16289  opeo  16290  omeo  16291  gcddvds  16428  gcdcl  16431  gcdeq0  16442  gcdneg  16447  gcdaddmlem  16449  bezoutlem3  16466  bezout  16468  gcddiv  16476  nn0rppwr  16486  eucalgval2  16506  lcmabs  16530  rpmul  16584  divgcdcoprmex  16591  isprm5  16632  prmexpb  16644  rpexp  16647  nn0gcdsq  16677  pcqmul  16779  prmreclem3  16844  mul4sq  16880  vdwapval  16899  f1ocpbl  17444  homfval  17613  comfval  17621  issect  17675  isfull  17834  isfth  17838  natfval  17871  catchom  18025  catcco  18027  funcsetcestrclem5  18080  plusfval  18570  0subm  18740  cycsubm  19129  cyccom  19130  isgim  19189  subgga  19227  cayleylem1  19339  lsmsubm  19580  subgdisjb  19620  pj1fval  19621  odadd1  19775  qusabl  19792  imasabl  19803  dprdsubg  19953  rnghmval  20374  isrngim  20379  dfrhm2  20408  isrhm  20412  isrim0  20416  rhmval  20431  funcrngcsetcALT  20572  srhmsubclem3  20610  srhmsubc  20611  fldhmsubc  20716  scafval  20830  rmodislmodlem  20878  rmodislmod  20879  lss1d  20912  islmhm  20977  islmim  21012  pzriprnglem5  21438  pzriprnglem8  21441  znfld  21513  cygznlem3  21522  cnmsgnsubg  21530  psgnghm  21533  ipeq0  21591  ipfval  21602  dsmmval  21687  dsmmacl  21694  mplval  21942  mplcoe5lem  21992  opsrval  21999  evlval  22053  mpfind  22068  selvffval  22074  mhpfval  22079  mhpmulcl  22090  psdffval  22098  mat1dimcrng  22419  dmatval  22434  dmatmulcl  22442  scmatval  22446  scmataddcl  22458  scmatsubcl  22459  scmatmulcl  22460  mavmul0g  22495  marrepfval  22502  marrepeval  22505  marepvfval  22507  marepveval  22510  submafval  22521  submaeval  22524  mdetfval  22528  madugsum  22585  minmar1fval  22588  minmar1eval  22591  symgmatr01  22596  gsummatr01lem3  22599  gsummatr01lem4  22600  gsummatr01  22601  cpmatacl  22658  mat2pmatfval  22665  mat2pmatvalel  22667  mat2pmatmul  22673  cpm2mfval  22691  cpm2mvalel  22693  m2cpminvid  22695  m2cpminvid2  22697  decpmate  22708  pmatcollpw1  22718  monmatcollpw  22721  pmatcollpwlem  22722  pmatcollpw  22723  pmatcollpwscmatlem2  22732  pm2mpval  22737  pm2mpf1  22741  mp2pm2mplem3  22750  mp2pm2mplem4  22751  chpmatfval  22772  tx2ndc  23593  cnmpt2t  23615  cnmpt22f  23617  hmeofval  23700  qustgplem  24063  stdbdmetval  24456  nmofval  24656  nghmfval  24664  isnmhm  24688  xrsxmet  24752  divcn  24813  divccn  24818  iihalf1cn  24880  iihalf2cn  24883  icchmeo  24892  cnrehmeo  24905  isphtpy  24934  isphtpc  24947  reparphti  24950  pcorevlem  24980  cphnm  25147  tcphnmval  25183  ipcau2  25188  tcphcphlem1  25189  tcphcphlem2  25190  tcphcph  25191  bcthlem1  25278  bcth  25283  mulcncf  25400  dyadmax  25553  volcn  25561  vitalilem1  25563  vitalilem2  25564  vitalilem3  25565  vitali  25568  i1fmullem  25649  itg1addlem4  25654  dvlip  25952  ftc1a  25998  mdegfval  26021  r1pval  26117  coeaddlem  26208  plycn  26220  quotval  26254  elqaalem2  26282  taylfval  26320  psercn2  26386  cxpcn  26708  cxpcn3  26712  resqrtcn  26713  sqrtcn  26714  abscxpbnd  26717  angval  26765  chordthmlem  26796  dcubic  26810  efrlim  26933  lgsdchr  27320  mul2sq  27384  ostthlem2  27593  zaddscl  28352  zmulscld  28355  zseo  28380  zs12addscl  28426  tglngval  28572  islnopp  28760  ishpg  28780  finsumvtxdg2size  29573  wspthsn  29870  wwlksnon  29873  wspthsnon  29874  iswspthsnon  29878  2clwwlk  30371  numclwlk1lem2  30394  numclwwlkovh0  30396  hmoval  30834  htth  30942  normval  31148  hlimi  31212  hsn0elch  31272  ocsh  31307  shscli  31341  shs00i  31474  chj00i  31511  riesz4i  32087  stm1addi  32269  stm1add3i  32271  superpos  32378  elrgspnlem2  33274  prmidlc  33478  idlsrgmulrval  33539  splyval  33666  brfinext  33758  finextfldext  33770  irngval  33791  minplyval  33811  submateq  33915  metidv  33998  rmulccn  34034  pl1cn  34061  sibfof  34446  cxpcncf1  34701  subfacval2  35330  txsconnlem  35383  cvxpconn  35385  cvxsconn  35386  iscvm  35402  prv  35571  mpomulnzcnf  36442  knoppcnlem10  36645  bj-bary1  37456  ismblfin  37801  itg2addnclem3  37813  itg2addnc  37814  ftc1anclem3  37835  ftc1anc  37841  bfp  37964  rngo2  38047  rngohomco  38114  rngoisoval  38117  rngoisocnv  38121  crngohomfo  38146  keridl  38172  ispridlc  38210  snatpsubN  39949  cdlemn11pre  41409  dihord2pre  41424  baerlem3lem1  41906  prjcrvfval  42816  mendval  43363  mendplusg  43366  omcl3g  43518  mulvval  44650  fprodcnlem  45787  climf  45810  climf2  45852  cxpcncf2  46085  smflimlem3  46959  fmtnofac2lem  47756  prmdvdsfmtnof1lem2  47773  opoeALTV  47871  opeoALTV  47872  rngchomALTV  48456  funcringcsetcALTV2lem5  48482  ringchomALTV  48490  funcringcsetclem5ALTV  48505  srhmsubcALTVlem2  48512  srhmsubcALTV  48513  fldhmsubcALTV  48521  dmatALTval  48588  lincsumcl  48619  fdivval  48727  catprslem  49197  catprsc  49200  catprsc2  49201  oppcendc  49205  thincmoALT  49616  functhinclem2  49632  fullthinc2  49638  setc1onsubc  49789  lmdfval  49836  cmdfval  49837