Theorem oveq12 7379

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

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510  df-ov 7373

This theorem is referenced by:  oveq12i  7382  oveq12d  7388  oveqan12d  7389  ovmpot  7531  mptmpoopabovd  8038  suppofssd  8157  sprmpod  8178  oev2  8462  oa00  8498  omopthi  8601  ecopoveq  8769  ecopovtrn  8771  isfsupp  9282  cantnffval  9586  ttrcltr  9639  fpwwe2lem4  10559  fpwwe2  10568  pwfseqlem4  10587  halfnq  10901  distrlem5pr  10952  addcmpblnr  10994  ltsrpr  11002  mulgt0sr  11030  add20  11663  msqge0  11672  recextlem2  11782  cru  12151  zaddcl  12545  qaddcl  12892  qmulcl  12894  xaddval  13152  xmulval  13154  xnn0xadd0  13176  xadddilem  13223  fzopth  13491  fzoopth  13692  modval  13805  1exp  14028  m1expeven  14046  nn0opthi  14207  faclbnd  14227  faclbnd3  14229  bcn0  14247  ccatopth  14653  ccatopth2  14654  repswccat  14723  reval  15043  absval  15175  clim  15431  rlim  15432  fsumparts  15743  cpnnen  16168  dvds2add  16231  dvds2sub  16232  opoe  16304  omoe  16305  opeo  16306  omeo  16307  gcddvds  16444  gcdcl  16447  gcdeq0  16458  gcdneg  16463  gcdaddmlem  16465  bezoutlem3  16482  bezout  16484  gcddiv  16492  nn0rppwr  16502  eucalgval2  16522  lcmabs  16546  rpmul  16600  divgcdcoprmex  16607  isprm5  16648  prmexpb  16660  rpexp  16663  nn0gcdsq  16693  pcqmul  16795  prmreclem3  16860  mul4sq  16896  vdwapval  16915  f1ocpbl  17460  homfval  17629  comfval  17637  issect  17691  isfull  17850  isfth  17854  natfval  17887  catchom  18041  catcco  18043  funcsetcestrclem5  18096  plusfval  18586  0subm  18756  cycsubm  19148  cyccom  19149  isgim  19208  subgga  19246  cayleylem1  19358  lsmsubm  19599  subgdisjb  19639  pj1fval  19640  odadd1  19794  qusabl  19811  imasabl  19822  dprdsubg  19972  rnghmval  20393  isrngim  20398  dfrhm2  20427  isrhm  20431  isrim0  20435  rhmval  20450  funcrngcsetcALT  20591  srhmsubclem3  20629  srhmsubc  20630  fldhmsubc  20735  scafval  20849  rmodislmodlem  20897  rmodislmod  20898  lss1d  20931  islmhm  20996  islmim  21031  pzriprnglem5  21457  pzriprnglem8  21460  znfld  21532  cygznlem3  21541  cnmsgnsubg  21549  psgnghm  21552  ipeq0  21610  ipfval  21621  dsmmval  21706  dsmmacl  21713  mplval  21961  mplcoe5lem  22011  opsrval  22018  evlval  22072  mpfind  22087  selvffval  22093  mhpfval  22098  mhpmulcl  22109  psdffval  22117  mat1dimcrng  22438  dmatval  22453  dmatmulcl  22461  scmatval  22465  scmataddcl  22477  scmatsubcl  22478  scmatmulcl  22479  mavmul0g  22514  marrepfval  22521  marrepeval  22524  marepvfval  22526  marepveval  22529  submafval  22540  submaeval  22543  mdetfval  22547  madugsum  22604  minmar1fval  22607  minmar1eval  22610  symgmatr01  22615  gsummatr01lem3  22618  gsummatr01lem4  22619  gsummatr01  22620  cpmatacl  22677  mat2pmatfval  22684  mat2pmatvalel  22686  mat2pmatmul  22692  cpm2mfval  22710  cpm2mvalel  22712  m2cpminvid  22714  m2cpminvid2  22716  decpmate  22727  pmatcollpw1  22737  monmatcollpw  22740  pmatcollpwlem  22741  pmatcollpw  22742  pmatcollpwscmatlem2  22751  pm2mpval  22756  pm2mpf1  22760  mp2pm2mplem3  22769  mp2pm2mplem4  22770  chpmatfval  22791  tx2ndc  23612  cnmpt2t  23634  cnmpt22f  23636  hmeofval  23719  qustgplem  24082  stdbdmetval  24475  nmofval  24675  nghmfval  24683  isnmhm  24707  xrsxmet  24771  divcn  24832  divccn  24837  iihalf1cn  24899  iihalf2cn  24902  icchmeo  24911  cnrehmeo  24924  isphtpy  24953  isphtpc  24966  reparphti  24969  pcorevlem  24999  cphnm  25166  tcphnmval  25202  ipcau2  25207  tcphcphlem1  25208  tcphcphlem2  25209  tcphcph  25210  bcthlem1  25297  bcth  25302  mulcncf  25419  dyadmax  25572  volcn  25580  vitalilem1  25582  vitalilem2  25583  vitalilem3  25584  vitali  25587  i1fmullem  25668  itg1addlem4  25673  dvlip  25971  ftc1a  26017  mdegfval  26040  r1pval  26136  coeaddlem  26227  plycn  26239  quotval  26273  elqaalem2  26301  taylfval  26339  psercn2  26405  cxpcn  26727  cxpcn3  26731  resqrtcn  26732  sqrtcn  26733  abscxpbnd  26736  angval  26784  chordthmlem  26815  dcubic  26829  efrlim  26952  lgsdchr  27339  mul2sq  27403  ostthlem2  27612  zaddscl  28407  zmulscld  28410  zseo  28435  z12addscl  28490  tglngval  28641  islnopp  28829  ishpg  28849  finsumvtxdg2size  29642  wspthsn  29939  wwlksnon  29942  wspthsnon  29943  iswspthsnon  29947  2clwwlk  30440  numclwlk1lem2  30463  numclwwlkovh0  30465  hmoval  30904  htth  31012  normval  31218  hlimi  31282  hsn0elch  31342  ocsh  31377  shscli  31411  shs00i  31544  chj00i  31581  riesz4i  32157  stm1addi  32339  stm1add3i  32341  superpos  32448  elrgspnlem2  33343  prmidlc  33547  idlsrgmulrval  33608  splyval  33742  brfinext  33836  finextfldext  33848  irngval  33869  minplyval  33889  submateq  33993  metidv  34076  rmulccn  34112  pl1cn  34139  sibfof  34524  cxpcncf1  34779  subfacval2  35409  txsconnlem  35462  cvxpconn  35464  cvxsconn  35465  iscvm  35481  prv  35650  mpomulnzcnf  36521  knoppcnlem10  36730  bj-bary1  37594  ismblfin  37941  itg2addnclem3  37953  itg2addnc  37954  ftc1anclem3  37975  ftc1anc  37981  bfp  38104  rngo2  38187  rngohomco  38254  rngoisoval  38257  rngoisocnv  38261  crngohomfo  38286  keridl  38312  ispridlc  38350  snatpsubN  40155  cdlemn11pre  41615  dihord2pre  41630  baerlem3lem1  42112  prjcrvfval  43018  mendval  43565  mendplusg  43568  omcl3g  43720  mulvval  44852  fprodcnlem  45988  climf  46011  climf2  46053  cxpcncf2  46286  smflimlem3  47160  fmtnofac2lem  47957  prmdvdsfmtnof1lem2  47974  opoeALTV  48072  opeoALTV  48073  rngchomALTV  48657  funcringcsetcALTV2lem5  48683  ringchomALTV  48691  funcringcsetclem5ALTV  48706  srhmsubcALTVlem2  48713  srhmsubcALTV  48714  fldhmsubcALTV  48722  dmatALTval  48789  lincsumcl  48820  fdivval  48928  catprslem  49398  catprsc  49401  catprsc2  49402  oppcendc  49406  thincmoALT  49817  functhinclem2  49833  fullthinc2  49839  setc1onsubc  49990  lmdfval  50037  cmdfval  50038