Theorem oveq12 7369

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

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

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  oveq12i  7372  oveq12d  7378  oveqan12d  7379  ovmpot  7521  mptmpoopabovd  8028  suppofssd  8147  sprmpod  8168  oev2  8452  oa00  8488  omopthi  8591  ecopoveq  8759  ecopovtrn  8761  isfsupp  9272  cantnffval  9576  ttrcltr  9629  fpwwe2lem4  10549  fpwwe2  10558  pwfseqlem4  10577  halfnq  10891  distrlem5pr  10942  addcmpblnr  10984  ltsrpr  10992  mulgt0sr  11020  add20  11653  msqge0  11662  recextlem2  11772  cru  12141  zaddcl  12535  qaddcl  12882  qmulcl  12884  xaddval  13142  xmulval  13144  xnn0xadd0  13166  xadddilem  13213  fzopth  13481  fzoopth  13682  modval  13795  1exp  14018  m1expeven  14036  nn0opthi  14197  faclbnd  14217  faclbnd3  14219  bcn0  14237  ccatopth  14643  ccatopth2  14644  repswccat  14713  reval  15033  absval  15165  clim  15421  rlim  15422  fsumparts  15733  cpnnen  16158  dvds2add  16221  dvds2sub  16222  opoe  16294  omoe  16295  opeo  16296  omeo  16297  gcddvds  16434  gcdcl  16437  gcdeq0  16448  gcdneg  16453  gcdaddmlem  16455  bezoutlem3  16472  bezout  16474  gcddiv  16482  nn0rppwr  16492  eucalgval2  16512  lcmabs  16536  rpmul  16590  divgcdcoprmex  16597  isprm5  16638  prmexpb  16650  rpexp  16653  nn0gcdsq  16683  pcqmul  16785  prmreclem3  16850  mul4sq  16886  vdwapval  16905  f1ocpbl  17450  homfval  17619  comfval  17627  issect  17681  isfull  17840  isfth  17844  natfval  17877  catchom  18031  catcco  18033  funcsetcestrclem5  18086  plusfval  18576  0subm  18746  cycsubm  19135  cyccom  19136  isgim  19195  subgga  19233  cayleylem1  19345  lsmsubm  19586  subgdisjb  19626  pj1fval  19627  odadd1  19781  qusabl  19798  imasabl  19809  dprdsubg  19959  rnghmval  20380  isrngim  20385  dfrhm2  20414  isrhm  20418  isrim0  20422  rhmval  20437  funcrngcsetcALT  20578  srhmsubclem3  20616  srhmsubc  20617  fldhmsubc  20722  scafval  20836  rmodislmodlem  20884  rmodislmod  20885  lss1d  20918  islmhm  20983  islmim  21018  pzriprnglem5  21444  pzriprnglem8  21447  znfld  21519  cygznlem3  21528  cnmsgnsubg  21536  psgnghm  21539  ipeq0  21597  ipfval  21608  dsmmval  21693  dsmmacl  21700  mplval  21948  mplcoe5lem  21998  opsrval  22005  evlval  22059  mpfind  22074  selvffval  22080  mhpfval  22085  mhpmulcl  22096  psdffval  22104  mat1dimcrng  22425  dmatval  22440  dmatmulcl  22448  scmatval  22452  scmataddcl  22464  scmatsubcl  22465  scmatmulcl  22466  mavmul0g  22501  marrepfval  22508  marrepeval  22511  marepvfval  22513  marepveval  22516  submafval  22527  submaeval  22530  mdetfval  22534  madugsum  22591  minmar1fval  22594  minmar1eval  22597  symgmatr01  22602  gsummatr01lem3  22605  gsummatr01lem4  22606  gsummatr01  22607  cpmatacl  22664  mat2pmatfval  22671  mat2pmatvalel  22673  mat2pmatmul  22679  cpm2mfval  22697  cpm2mvalel  22699  m2cpminvid  22701  m2cpminvid2  22703  decpmate  22714  pmatcollpw1  22724  monmatcollpw  22727  pmatcollpwlem  22728  pmatcollpw  22729  pmatcollpwscmatlem2  22738  pm2mpval  22743  pm2mpf1  22747  mp2pm2mplem3  22756  mp2pm2mplem4  22757  chpmatfval  22778  tx2ndc  23599  cnmpt2t  23621  cnmpt22f  23623  hmeofval  23706  qustgplem  24069  stdbdmetval  24462  nmofval  24662  nghmfval  24670  isnmhm  24694  xrsxmet  24758  divcn  24819  divccn  24824  iihalf1cn  24886  iihalf2cn  24889  icchmeo  24898  cnrehmeo  24911  isphtpy  24940  isphtpc  24953  reparphti  24956  pcorevlem  24986  cphnm  25153  tcphnmval  25189  ipcau2  25194  tcphcphlem1  25195  tcphcphlem2  25196  tcphcph  25197  bcthlem1  25284  bcth  25289  mulcncf  25406  dyadmax  25559  volcn  25567  vitalilem1  25569  vitalilem2  25570  vitalilem3  25571  vitali  25574  i1fmullem  25655  itg1addlem4  25660  dvlip  25958  ftc1a  26004  mdegfval  26027  r1pval  26123  coeaddlem  26214  plycn  26226  quotval  26260  elqaalem2  26288  taylfval  26326  psercn2  26392  cxpcn  26714  cxpcn3  26718  resqrtcn  26719  sqrtcn  26720  abscxpbnd  26723  angval  26771  chordthmlem  26802  dcubic  26816  efrlim  26939  lgsdchr  27326  mul2sq  27390  ostthlem2  27599  zaddscl  28394  zmulscld  28397  zseo  28422  z12addscl  28477  tglngval  28627  islnopp  28815  ishpg  28835  finsumvtxdg2size  29628  wspthsn  29925  wwlksnon  29928  wspthsnon  29929  iswspthsnon  29933  2clwwlk  30426  numclwlk1lem2  30449  numclwwlkovh0  30451  hmoval  30889  htth  30997  normval  31203  hlimi  31267  hsn0elch  31327  ocsh  31362  shscli  31396  shs00i  31529  chj00i  31566  riesz4i  32142  stm1addi  32324  stm1add3i  32326  superpos  32433  elrgspnlem2  33327  prmidlc  33531  idlsrgmulrval  33592  splyval  33719  brfinext  33811  finextfldext  33823  irngval  33844  minplyval  33864  submateq  33968  metidv  34051  rmulccn  34087  pl1cn  34114  sibfof  34499  cxpcncf1  34754  subfacval2  35383  txsconnlem  35436  cvxpconn  35438  cvxsconn  35439  iscvm  35455  prv  35624  mpomulnzcnf  36495  knoppcnlem10  36704  bj-bary1  37519  ismblfin  37864  itg2addnclem3  37876  itg2addnc  37877  ftc1anclem3  37898  ftc1anc  37904  bfp  38027  rngo2  38110  rngohomco  38177  rngoisoval  38180  rngoisocnv  38184  crngohomfo  38209  keridl  38235  ispridlc  38273  snatpsubN  40078  cdlemn11pre  41538  dihord2pre  41553  baerlem3lem1  42035  prjcrvfval  42941  mendval  43488  mendplusg  43491  omcl3g  43643  mulvval  44775  fprodcnlem  45912  climf  45935  climf2  45977  cxpcncf2  46210  smflimlem3  47084  fmtnofac2lem  47881  prmdvdsfmtnof1lem2  47898  opoeALTV  47996  opeoALTV  47997  rngchomALTV  48581  funcringcsetcALTV2lem5  48607  ringchomALTV  48615  funcringcsetclem5ALTV  48630  srhmsubcALTVlem2  48637  srhmsubcALTV  48638  fldhmsubcALTV  48646  dmatALTval  48713  lincsumcl  48744  fdivval  48852  catprslem  49322  catprsc  49325  catprsc2  49326  oppcendc  49330  thincmoALT  49741  functhinclem2  49757  fullthinc2  49763  setc1onsubc  49914  lmdfval  49961  cmdfval  49962