Theorem oveq12 7410

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1533  (class class class)co 7401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-iota 6485  df-fv 6541  df-ov 7404

This theorem is referenced by:  oveq12i  7413  oveq12d  7419  oveqan12d  7420  ovmpot  7561  mptmpoopabovd  8062  mptmpoopabovdOLD  8064  suppofssd  8183  sprmpod  8204  oev2  8518  oa00  8554  omopthi  8655  ecopoveq  8807  ecopovtrn  8809  isfsupp  9360  cantnffval  9653  ttrcltr  9706  fpwwe2  10633  halfnq  10966  distrlem5pr  11017  addcmpblnr  11059  ltsrpr  11067  mulgt0sr  11095  add20  11722  msqge0  11731  recextlem2  11841  cru  12200  zaddcl  12598  qaddcl  12945  qmulcl  12947  xaddval  13198  xmulval  13200  xnn0xadd0  13222  xadddilem  13269  fzopth  13534  modval  13832  1exp  14053  m1expeven  14071  nn0opthi  14226  faclbnd  14246  faclbnd3  14248  bcn0  14266  ccatopth  14662  ccatopth2  14663  repswccat  14732  reval  15049  absval  15181  clim  15434  rlim  15435  fsumparts  15748  cpnnen  16168  dvds2add  16229  dvds2sub  16230  opoe  16302  omoe  16303  opeo  16304  omeo  16305  gcddvds  16440  gcdcl  16443  gcdeq0  16454  gcdneg  16459  gcdaddmlem  16461  gcdabsOLD  16469  bezoutlem3  16479  bezout  16481  gcddiv  16489  eucalgval2  16514  lcmabs  16538  rpmul  16592  divgcdcoprmex  16599  isprm5  16640  prmexpb  16653  rpexp  16656  nn0gcdsq  16686  pcqmul  16784  prmreclem3  16849  mul4sq  16885  vdwapval  16904  f1ocpbl  17469  homfval  17634  comfval  17642  issect  17698  isfull  17861  isfth  17865  natfval  17898  catchom  18054  catcco  18056  funcsetcestrclem5  18112  plusfval  18569  0subm  18731  cycsubm  19117  cyccom  19118  isgim  19176  subgga  19205  cayleylem1  19321  lsmsubm  19562  subgdisjb  19602  pj1fval  19603  odadd1  19757  qusabl  19774  imasabl  19785  dprdsubg  19935  rnghmval  20331  isrngim  20336  dfrhm2  20365  isrhm  20369  isrim0OLD  20372  isrim0  20374  rhmval  20391  funcrngcsetcALT  20526  srhmsubclem3  20564  srhmsubc  20565  fldhmsubc  20625  scafval  20716  rmodislmodlem  20764  rmodislmod  20765  rmodislmodOLD  20766  lss1d  20799  islmhm  20864  islmim  20899  pzriprnglem5  21339  pzriprnglem8  21342  znfld  21422  cygznlem3  21431  cnmsgnsubg  21437  psgnghm  21440  ipeq0  21498  ipfval  21509  dsmmval  21596  dsmmacl  21603  mplval  21857  mplcoe5lem  21903  opsrval  21910  evlval  21967  mpfind  21979  selvffval  21985  mhpfval  21989  mhpmulcl  21999  psdffval  22007  mat1dimcrng  22300  dmatval  22315  dmatmulcl  22323  scmatval  22327  scmataddcl  22339  scmatsubcl  22340  scmatmulcl  22341  mavmul0g  22376  marrepfval  22383  marrepeval  22386  marepvfval  22388  marepveval  22391  submafval  22402  submaeval  22405  mdetfval  22409  madugsum  22466  minmar1fval  22469  minmar1eval  22472  symgmatr01  22477  gsummatr01lem3  22480  gsummatr01lem4  22481  gsummatr01  22482  cpmatacl  22539  mat2pmatfval  22546  mat2pmatvalel  22548  mat2pmatmul  22554  cpm2mfval  22572  cpm2mvalel  22574  m2cpminvid  22576  m2cpminvid2  22578  decpmate  22589  pmatcollpw1  22599  monmatcollpw  22602  pmatcollpwlem  22603  pmatcollpw  22604  pmatcollpwscmatlem2  22613  pm2mpval  22618  pm2mpf1  22622  mp2pm2mplem3  22631  mp2pm2mplem4  22632  chpmatfval  22653  tx2ndc  23476  cnmpt2t  23498  cnmpt22f  23500  hmeofval  23583  qustgplem  23946  stdbdmetval  24344  nmofval  24552  nghmfval  24560  isnmhm  24584  xrsxmet  24646  divcn  24707  divccn  24712  iihalf1cn  24774  iihalf2cn  24777  icchmeo  24786  cnrehmeo  24799  isphtpy  24828  isphtpc  24841  reparphti  24844  pcorevlem  24874  cphnm  25042  tcphnmval  25078  ipcau2  25083  tcphcphlem1  25084  tcphcphlem2  25085  tcphcph  25086  bcthlem1  25173  bcth  25178  mulcncf  25295  dyadmax  25448  volcn  25456  vitalilem1  25458  vitalilem2  25459  vitalilem3  25460  vitali  25463  i1fmullem  25544  itg1addlem4  25549  itg1addlem4OLD  25550  dvlip  25847  ftc1a  25893  mdegfval  25919  r1pval  26013  coeaddlem  26102  plycn  26114  quotval  26145  elqaalem2  26173  taylfval  26211  psercn2  26275  cxpcn  26594  cxpcn3  26598  resqrtcn  26599  sqrtcn  26600  abscxpbnd  26603  angval  26648  chordthmlem  26679  dcubic  26693  efrlim  26816  lgsdchr  27203  mul2sq  27267  ostthlem2  27476  tglngval  28237  islnopp  28425  ishpg  28445  finsumvtxdg2size  29242  wspthsn  29537  wwlksnon  29540  wspthsnon  29541  iswspthsnon  29545  2clwwlk  30035  numclwlk1lem2  30058  numclwwlkovh0  30060  hmoval  30498  htth  30606  normval  30812  hlimi  30876  hsn0elch  30936  ocsh  30971  shscli  31005  shs00i  31138  chj00i  31175  riesz4i  31751  stm1addi  31933  stm1add3i  31935  superpos  32042  prmidlc  33002  idlsrgmulrval  33058  brfinext  33177  irngval  33195  minplyval  33212  submateq  33244  metidv  33327  rmulccn  33363  pl1cn  33390  sibfof  33794  cxpcncf1  34062  subfacval2  34633  txsconnlem  34686  cvxpconn  34688  cvxsconn  34689  iscvm  34705  prv  34874  mpomulnzcnf  35620  knoppcnlem10  35834  bj-bary1  36649  ismblfin  36985  itg2addnclem3  36997  itg2addnc  36998  ftc1anclem3  37019  ftc1anc  37025  bfp  37148  rngo2  37231  rngohomco  37298  rngoisoval  37301  rngoisocnv  37305  crngohomfo  37330  keridl  37356  ispridlc  37394  snatpsubN  39077  cdlemn11pre  40537  dihord2pre  40552  baerlem3lem1  41034  nn0rppwr  41679  sn-inelr  41793  prjcrvfval  41828  mendval  42380  mendplusg  42383  omcl3g  42539  mulvval  43682  fprodcnlem  44766  climf  44789  climf2  44833  cxpcncf2  45066  smflimlem3  45940  fzoopth  46486  fmtnofac2lem  46687  prmdvdsfmtnof1lem2  46704  opoeALTV  46802  opeoALTV  46803  rngchomALTV  47097  funcringcsetcALTV2lem5  47123  ringchomALTV  47131  funcringcsetclem5ALTV  47146  srhmsubcALTVlem2  47153  srhmsubcALTV  47154  fldhmsubcALTV  47162  dmatALTval  47235  lincsumcl  47266  fdivval  47379  catprslem  47784  catprsc  47787  catprsc2  47788  thincmoALT  47804  functhinclem2  47816  fullthinc2  47821