Theorem oveq12 7407

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1562  (class class class)co 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-iota 6479  df-fv 6531  df-ov 7401

This theorem is referenced by:  oveq12i  7410  oveq12d  7416  oveqan12d  7417  ovmpot  7559  mptmpoopabovd  8065  suppofssd  8185  sprmpod  8206  oev2  8494  oa00  8530  omopthi  8633  ecopoveq  8802  ecopovtrn  8804  isfsupp  9313  cantnffval  9620  ttrcltr  9673  fpwwe2lem4  10594  fpwwe2  10603  pwfseqlem4  10622  halfnq  10936  distrlem5pr  10987  addcmpblnr  11029  ltsrpr  11037  mulgt0sr  11065  add20  11701  msqge0  11710  recextlem2  11820  cru  12189  zaddcl  12613  qaddcl  12968  qmulcl  12970  xaddval  13228  xmulval  13230  xnn0xadd0  13252  xadddilem  13299  fzopth  13568  fzoopth  13770  modval  13883  1exp  14106  m1expeven  14124  nn0opthi  14285  faclbnd  14305  faclbnd3  14307  bcn0  14325  ccatopth  14731  ccatopth2  14732  repswccat  14801  reval  15135  absval  15267  clim  15523  rlim  15524  fsumparts  15836  cpnnen  16263  dvds2add  16326  dvds2sub  16327  opoe  16399  omoe  16400  opeo  16401  omeo  16402  gcddvds  16539  gcdcl  16542  gcdeq0  16553  gcdneg  16558  gcdaddmlem  16560  bezoutlem3  16577  bezout  16579  gcddiv  16587  nn0rppwr  16597  eucalgval2  16617  lcmabs  16641  rpmul  16695  divgcdcoprmex  16702  isprm5  16744  prmexpb  16756  rpexp  16759  nn0gcdsq  16789  pcqmul  16891  prmreclem3  16956  mul4sq  16992  vdwapval  17011  f1ocpbl  17557  homfval  17726  comfval  17734  issect  17788  isfull  17947  isfth  17951  natfval  17984  catchom  18138  catcco  18140  funcsetcestrclem5  18193  plusfval  18683  0subm  18853  cycsubm  19245  cyccom  19246  isgim  19304  subgga  19342  cayleylem1  19454  lsmsubm  19695  subgdisjb  19735  pj1fval  19736  odadd1  19890  qusabl  19907  imasabl  19918  dprdsubg  20068  rnghmval  20491  isrngim  20496  dfrhm2  20525  isrhm  20529  isrim0  20533  rhmval  20551  funcrngcsetcALT  20693  srhmsubclem3  20731  srhmsubc  20732  fldhmsubc  20836  scafval  20950  rmodislmodlem  20998  rmodislmod  20999  lss1d  21032  islmhm  21096  islmim  21131  pzriprnglem5  21539  pzriprnglem8  21542  znfld  21614  cygznlem3  21623  cnmsgnsubg  21631  psgnghm  21634  ipeq0  21692  ipfval  21703  dsmmval  21788  dsmmacl  21795  mplval  22042  mplcoe5lem  22094  opsrval  22101  evlval  22155  mpfind  22170  selvffval  22173  mhpfval  22205  mhpmulcl  22216  psdffval  22224  mat1dimcrng  22539  dmatval  22554  dmatmulcl  22562  scmatval  22566  scmataddcl  22578  scmatsubcl  22579  scmatmulcl  22580  mavmul0g  22615  marrepfval  22622  marrepeval  22625  marepvfval  22627  marepveval  22630  submafval  22641  submaeval  22644  mdetfval  22648  madugsum  22705  minmar1fval  22708  minmar1eval  22711  symgmatr01  22716  gsummatr01lem3  22719  gsummatr01lem4  22720  gsummatr01  22721  cpmatacl  22778  mat2pmatfval  22785  mat2pmatvalel  22787  mat2pmatmul  22793  cpm2mfval  22811  cpm2mvalel  22813  m2cpminvid  22815  m2cpminvid2  22817  decpmate  22828  pmatcollpw1  22838  monmatcollpw  22841  pmatcollpwlem  22842  pmatcollpw  22843  pmatcollpwscmatlem2  22852  pm2mpval  22857  pm2mpf1  22861  mp2pm2mplem3  22870  mp2pm2mplem4  22871  chpmatfval  22892  tx2ndc  23713  cnmpt2t  23735  cnmpt22f  23737  hmeofval  23820  qustgplem  24183  stdbdmetval  24576  nmofval  24776  nghmfval  24784  isnmhm  24808  xrsxmet  24872  divcn  24932  divccn  24937  iihalf1cn  24996  iihalf2cn  24998  icchmeo  25005  cnrehmeo  25017  isphtpy  25045  isphtpc  25058  reparphti  25061  pcorevlem  25090  cphnm  25257  tcphnmval  25293  ipcau2  25298  tcphcphlem1  25299  tcphcphlem2  25300  tcphcph  25301  bcthlem1  25388  bcth  25393  mulcncf  25510  dyadmax  25662  volcn  25670  vitalilem1  25672  vitalilem2  25673  vitalilem3  25674  vitali  25677  i1fmullem  25758  itg1addlem4  25763  dvlip  26057  ftc1a  26101  mdegfval  26124  r1pval  26220  coeaddlem  26311  plycn  26323  quotval  26358  elqaalem2  26386  taylfval  26424  psercn2  26488  cxpcn  26812  cxpcn3  26815  resqrtcn  26816  sqrtcn  26817  abscxpbnd  26820  angval  26868  chordthmlem  26899  dcubic  26913  efrlim  27036  lgsdchr  27421  mul2sq  27485  ostthlem2  27694  zaddscl  28489  zmulscld  28492  zseo  28517  z12addscl  28572  tglngval  28722  islnopp  28914  ishpg  28934  elplngid  28991  lnincplng  28993  plngcp  28995  plngrot  28999  finsumvtxdg2size  29753  wspthsn  30050  wwlksnon  30053  wspthsnon  30054  iswspthsnon  30058  2clwwlk  30551  numclwlk1lem2  30574  numclwwlkovh0  30576  hmoval  31015  htth  31123  normval  31329  hlimi  31393  hsn0elch  31453  ocsh  31488  shscli  31522  shs00i  31655  chj00i  31692  riesz4i  32268  stm1addi  32450  stm1add3i  32452  superpos  32559  elrgspnlem2  33426  prmidlc  33636  drnglring  33690  idlsrgmulrval  33707  splyval  33858  brfinext  33951  finextfldext  33963  irngval  33984  minplyval  34004  submateq  34108  metidv  34191  rmulccn  34227  pl1cn  34254  sibfof  34639  cxpcncf1  34891  subfacval2  35542  txsconnlem  35595  cvxpconn  35597  cvxsconn  35598  iscvm  35614  prv  35783  mpomulnzcnf  36664  knoppcnlem10  36945  bj-bary1  37809  ismblfin  38165  itg2addnclem3  38177  itg2addnc  38178  ftc1anclem3  38199  ftc1anc  38205  bfp  38328  rngo2  38411  rngohomco  38478  rngoisoval  38481  rngoisocnv  38485  crngohomfo  38510  keridl  38536  ispridlc  38574  snatpsubN  40379  cdlemn11pre  41839  dihord2pre  41854  baerlem3lem1  42336  prjcrvfval  43218  mendval  43761  mendplusg  43764  omcl3g  43916  mulvval  45048  fprodcnlem  46180  climf  46203  climf2  46245  cxpcncf2  46478  smflimlem3  47352  fmtnofac2lem  48182  prmdvdsfmtnof1lem2  48199  opoeALTV  48310  opeoALTV  48311  rngchomALTV  48895  funcringcsetcALTV2lem5  48921  ringchomALTV  48929  funcringcsetclem5ALTV  48944  srhmsubcALTVlem2  48951  srhmsubcALTV  48952  fldhmsubcALTV  48960  dmatALTval  49027  lincsumcl  49058  fdivval  49166  catprslem  49636  catprsc  49639  catprsc2  49640  oppcendc  49644  thincmoALT  50055  functhinclem2  50071  fullthinc2  50077  setc1onsubc  50228  lmdfval  50275  cmdfval  50276