Theorem oveq12 7293

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  (class class class)co 7284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287

This theorem is referenced by:  oveq12i  7296  oveq12d  7302  oveqan12d  7303  mptmpoopabovd  7931  mptmpoopabovdOLD  7933  suppofssd  8028  sprmpod  8049  oev2  8362  oa00  8399  omopthi  8500  ecopoveq  8616  ecopovtrn  8618  isfsupp  9141  cantnffval  9430  ttrcltr  9483  fpwwe2  10408  halfnq  10741  distrlem5pr  10792  addcmpblnr  10834  ltsrpr  10842  mulgt0sr  10870  add20  11496  msqge0  11505  recextlem2  11615  cru  11974  zaddcl  12369  qaddcl  12714  qmulcl  12716  xaddval  12966  xmulval  12968  xnn0xadd0  12990  xadddilem  13037  fzopth  13302  modval  13600  1exp  13821  m1expeven  13839  nn0opthi  13993  faclbnd  14013  faclbnd3  14015  bcn0  14033  ccatopth  14438  ccatopth2  14439  repswccat  14508  reval  14826  absval  14958  clim  15212  rlim  15213  fsumparts  15527  cpnnen  15947  dvds2add  16008  dvds2sub  16009  opoe  16081  omoe  16082  opeo  16083  omeo  16084  gcddvds  16219  gcdcl  16222  gcdeq0  16233  gcdneg  16238  gcdaddmlem  16240  gcdabsOLD  16248  bezoutlem3  16258  bezout  16260  gcddiv  16268  eucalgval2  16295  lcmabs  16319  rpmul  16373  divgcdcoprmex  16380  isprm5  16421  prmexpb  16434  rpexp  16436  nn0gcdsq  16465  pcqmul  16563  prmreclem3  16628  mul4sq  16664  vdwapval  16683  f1ocpbl  17245  homfval  17410  comfval  17418  issect  17474  isfull  17635  isfth  17639  natfval  17671  catchom  17827  catcco  17829  funcsetcestrclem5  17885  plusfval  18342  0subm  18465  cycsubm  18830  cyccom  18831  isgim  18887  subgga  18915  cayleylem1  19029  lsmsubm  19267  subgdisjb  19308  pj1fval  19309  odadd1  19458  qusabl  19475  cygablOLD  19501  dprdsubg  19636  ringadd2  19823  dfrhm2  19970  isrhm  19974  isrim0  19976  scafval  20151  rmodislmodlem  20199  rmodislmod  20200  rmodislmodOLD  20201  lss1d  20234  islmhm  20298  islmim  20333  znfld  20777  cygznlem3  20786  cnmsgnsubg  20791  psgnghm  20794  ipeq0  20852  ipfval  20863  dsmmval  20950  dsmmacl  20957  mplval  21206  mplcoe5lem  21249  opsrval  21256  evlval  21314  mpfind  21326  selvffval  21335  mhpfval  21338  mhpmulcl  21348  mat1dimcrng  21635  dmatval  21650  dmatmulcl  21658  scmatval  21662  scmataddcl  21674  scmatsubcl  21675  scmatmulcl  21676  mavmul0g  21711  marrepfval  21718  marrepeval  21721  marepvfval  21723  marepveval  21726  submafval  21737  submaeval  21740  mdetfval  21744  madugsum  21801  minmar1fval  21804  minmar1eval  21807  symgmatr01  21812  gsummatr01lem3  21815  gsummatr01lem4  21816  gsummatr01  21817  cpmatacl  21874  mat2pmatfval  21881  mat2pmatvalel  21883  mat2pmatmul  21889  cpm2mfval  21907  cpm2mvalel  21909  m2cpminvid  21911  m2cpminvid2  21913  decpmate  21924  pmatcollpw1  21934  monmatcollpw  21937  pmatcollpwlem  21938  pmatcollpw  21939  pmatcollpwscmatlem2  21948  pm2mpval  21953  pm2mpf1  21957  mp2pm2mplem3  21966  mp2pm2mplem4  21967  chpmatfval  21988  tx2ndc  22811  cnmpt2t  22833  cnmpt22f  22835  hmeofval  22918  qustgplem  23281  stdbdmetval  23679  nmofval  23887  nghmfval  23895  isnmhm  23919  xrsxmet  23981  isphtpy  24153  isphtpc  24166  pcorevlem  24198  cphnm  24366  tcphnmval  24402  ipcau2  24407  tcphcphlem1  24408  tcphcphlem2  24409  tcphcph  24410  bcthlem1  24497  bcth  24502  dyadmax  24771  volcn  24779  vitalilem1  24781  vitalilem2  24782  vitalilem3  24783  vitali  24786  i1fmullem  24867  itg1addlem4  24872  itg1addlem4OLD  24873  dvlip  25166  ftc1a  25210  mdegfval  25236  r1pval  25330  coeaddlem  25419  quotval  25461  elqaalem2  25489  taylfval  25527  cxpcn3  25910  resqrtcn  25911  sqrtcn  25912  abscxpbnd  25915  angval  25960  chordthmlem  25991  dcubic  26005  lgsdchr  26512  mul2sq  26576  ostthlem2  26785  tglngval  26921  islnopp  27109  ishpg  27129  finsumvtxdg2size  27926  wspthsn  28222  wwlksnon  28225  wspthsnon  28226  iswspthsnon  28230  2clwwlk  28720  numclwlk1lem2  28743  numclwwlkovh0  28745  hmoval  29181  htth  29289  normval  29495  hlimi  29559  hsn0elch  29619  ocsh  29654  shscli  29688  shs00i  29821  chj00i  29858  riesz4i  30434  stm1addi  30616  stm1add3i  30618  superpos  30725  prmidlc  31633  idlsrgmulrval  31663  brfinext  31737  submateq  31768  metidv  31851  rmulccn  31887  pl1cn  31914  sibfof  32316  cxpcncf1  32584  subfacval2  33158  txsconnlem  33211  iscvm  33230  prv  33399  bj-bary1  35492  ismblfin  35827  itg2addnclem3  35839  itg2addnc  35840  ftc1anclem3  35861  ftc1anc  35867  bfp  35991  rngo2  36074  rngohomco  36141  rngoisoval  36144  rngoisocnv  36148  crngohomfo  36173  keridl  36199  ispridlc  36237  snatpsubN  37771  cdlemn11pre  39231  dihord2pre  39246  baerlem3lem1  39728  nn0rppwr  40340  sn-inelr  40442  prjcrvfval  40475  mendval  41015  mendplusg  41018  mulvval  42093  climf  43170  climf2  43214  cxpcncf2  43447  smflimlem3  44318  fzoopth  44830  fmtnofac2lem  45031  prmdvdsfmtnof1lem2  45048  opoeALTV  45146  opeoALTV  45147  rnghmval  45460  isrngisom  45465  rhmval  45488  rngchomALTV  45554  funcrngcsetcALT  45568  funcringcsetcALTV2lem5  45609  ringchomALTV  45617  funcringcsetclem5ALTV  45632  srhmsubclem3  45644  srhmsubc  45645  fldhmsubc  45653  srhmsubcALTVlem2  45662  srhmsubcALTV  45663  fldhmsubcALTV  45671  dmatALTval  45752  lincsumcl  45783  fdivval  45896  catprslem  46302  catprsc  46305  catprsc2  46306  thincmoALT  46322  functhinclem2  46334  fullthinc2  46339