Theorem oveq12 7355

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  oveq12i  7358  oveq12d  7364  oveqan12d  7365  ovmpot  7507  mptmpoopabovd  8014  suppofssd  8133  sprmpod  8154  oev2  8438  oa00  8474  omopthi  8576  ecopoveq  8742  ecopovtrn  8744  isfsupp  9249  cantnffval  9553  ttrcltr  9606  fpwwe2lem4  10525  fpwwe2  10534  pwfseqlem4  10553  halfnq  10867  distrlem5pr  10918  addcmpblnr  10960  ltsrpr  10968  mulgt0sr  10996  add20  11629  msqge0  11638  recextlem2  11748  cru  12117  zaddcl  12512  qaddcl  12863  qmulcl  12865  xaddval  13122  xmulval  13124  xnn0xadd0  13146  xadddilem  13193  fzopth  13461  fzoopth  13662  modval  13775  1exp  13998  m1expeven  14016  nn0opthi  14177  faclbnd  14197  faclbnd3  14199  bcn0  14217  ccatopth  14623  ccatopth2  14624  repswccat  14693  reval  15013  absval  15145  clim  15401  rlim  15402  fsumparts  15713  cpnnen  16138  dvds2add  16201  dvds2sub  16202  opoe  16274  omoe  16275  opeo  16276  omeo  16277  gcddvds  16414  gcdcl  16417  gcdeq0  16428  gcdneg  16433  gcdaddmlem  16435  bezoutlem3  16452  bezout  16454  gcddiv  16462  nn0rppwr  16472  eucalgval2  16492  lcmabs  16516  rpmul  16570  divgcdcoprmex  16577  isprm5  16618  prmexpb  16630  rpexp  16633  nn0gcdsq  16663  pcqmul  16765  prmreclem3  16830  mul4sq  16866  vdwapval  16885  f1ocpbl  17429  homfval  17598  comfval  17606  issect  17660  isfull  17819  isfth  17823  natfval  17856  catchom  18010  catcco  18012  funcsetcestrclem5  18065  plusfval  18555  0subm  18725  cycsubm  19114  cyccom  19115  isgim  19174  subgga  19212  cayleylem1  19324  lsmsubm  19565  subgdisjb  19605  pj1fval  19606  odadd1  19760  qusabl  19777  imasabl  19788  dprdsubg  19938  rnghmval  20358  isrngim  20363  dfrhm2  20392  isrhm  20396  isrim0  20400  rhmval  20415  funcrngcsetcALT  20556  srhmsubclem3  20594  srhmsubc  20595  fldhmsubc  20700  scafval  20814  rmodislmodlem  20862  rmodislmod  20863  lss1d  20896  islmhm  20961  islmim  20996  pzriprnglem5  21422  pzriprnglem8  21425  znfld  21497  cygznlem3  21506  cnmsgnsubg  21514  psgnghm  21517  ipeq0  21575  ipfval  21586  dsmmval  21671  dsmmacl  21678  mplval  21926  mplcoe5lem  21974  opsrval  21981  evlval  22030  mpfind  22042  selvffval  22048  mhpfval  22053  mhpmulcl  22064  psdffval  22072  mat1dimcrng  22392  dmatval  22407  dmatmulcl  22415  scmatval  22419  scmataddcl  22431  scmatsubcl  22432  scmatmulcl  22433  mavmul0g  22468  marrepfval  22475  marrepeval  22478  marepvfval  22480  marepveval  22483  submafval  22494  submaeval  22497  mdetfval  22501  madugsum  22558  minmar1fval  22561  minmar1eval  22564  symgmatr01  22569  gsummatr01lem3  22572  gsummatr01lem4  22573  gsummatr01  22574  cpmatacl  22631  mat2pmatfval  22638  mat2pmatvalel  22640  mat2pmatmul  22646  cpm2mfval  22664  cpm2mvalel  22666  m2cpminvid  22668  m2cpminvid2  22670  decpmate  22681  pmatcollpw1  22691  monmatcollpw  22694  pmatcollpwlem  22695  pmatcollpw  22696  pmatcollpwscmatlem2  22705  pm2mpval  22710  pm2mpf1  22714  mp2pm2mplem3  22723  mp2pm2mplem4  22724  chpmatfval  22745  tx2ndc  23566  cnmpt2t  23588  cnmpt22f  23590  hmeofval  23673  qustgplem  24036  stdbdmetval  24429  nmofval  24629  nghmfval  24637  isnmhm  24661  xrsxmet  24725  divcn  24786  divccn  24791  iihalf1cn  24853  iihalf2cn  24856  icchmeo  24865  cnrehmeo  24878  isphtpy  24907  isphtpc  24920  reparphti  24923  pcorevlem  24953  cphnm  25120  tcphnmval  25156  ipcau2  25161  tcphcphlem1  25162  tcphcphlem2  25163  tcphcph  25164  bcthlem1  25251  bcth  25256  mulcncf  25373  dyadmax  25526  volcn  25534  vitalilem1  25536  vitalilem2  25537  vitalilem3  25538  vitali  25541  i1fmullem  25622  itg1addlem4  25627  dvlip  25925  ftc1a  25971  mdegfval  25994  r1pval  26090  coeaddlem  26181  plycn  26193  quotval  26227  elqaalem2  26255  taylfval  26293  psercn2  26359  cxpcn  26681  cxpcn3  26685  resqrtcn  26686  sqrtcn  26687  abscxpbnd  26690  angval  26738  chordthmlem  26769  dcubic  26783  efrlim  26906  lgsdchr  27293  mul2sq  27357  ostthlem2  27566  zaddscl  28318  zmulscld  28321  zseo  28345  zs12addscl  28387  tglngval  28529  islnopp  28717  ishpg  28737  finsumvtxdg2size  29529  wspthsn  29826  wwlksnon  29829  wspthsnon  29830  iswspthsnon  29834  2clwwlk  30327  numclwlk1lem2  30350  numclwwlkovh0  30352  hmoval  30790  htth  30898  normval  31104  hlimi  31168  hsn0elch  31228  ocsh  31263  shscli  31297  shs00i  31430  chj00i  31467  riesz4i  32043  stm1addi  32225  stm1add3i  32227  superpos  32334  elrgspnlem2  33210  prmidlc  33413  idlsrgmulrval  33474  splyval  33582  brfinext  33665  finextfldext  33677  irngval  33698  minplyval  33718  submateq  33822  metidv  33905  rmulccn  33941  pl1cn  33968  sibfof  34353  cxpcncf1  34608  subfacval2  35231  txsconnlem  35284  cvxpconn  35286  cvxsconn  35287  iscvm  35303  prv  35472  mpomulnzcnf  36343  knoppcnlem10  36546  bj-bary1  37356  ismblfin  37700  itg2addnclem3  37712  itg2addnc  37713  ftc1anclem3  37734  ftc1anc  37740  bfp  37863  rngo2  37946  rngohomco  38013  rngoisoval  38016  rngoisocnv  38020  crngohomfo  38045  keridl  38071  ispridlc  38109  snatpsubN  39848  cdlemn11pre  41308  dihord2pre  41323  baerlem3lem1  41805  prjcrvfval  42723  mendval  43271  mendplusg  43274  omcl3g  43426  mulvval  44559  fprodcnlem  45698  climf  45721  climf2  45763  cxpcncf2  45996  smflimlem3  46870  fmtnofac2lem  47667  prmdvdsfmtnof1lem2  47684  opoeALTV  47782  opeoALTV  47783  rngchomALTV  48367  funcringcsetcALTV2lem5  48393  ringchomALTV  48401  funcringcsetclem5ALTV  48416  srhmsubcALTVlem2  48423  srhmsubcALTV  48424  fldhmsubcALTV  48432  dmatALTval  48500  lincsumcl  48531  fdivval  48639  catprslem  49110  catprsc  49113  catprsc2  49114  oppcendc  49118  thincmoALT  49529  functhinclem2  49545  fullthinc2  49551  setc1onsubc  49702  lmdfval  49749  cmdfval  49750