Theorem oveq12 7425

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  (class class class)co 7416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6491  df-fv 6543  df-ov 7419

This theorem is used by:  oveq12i  7428  oveq12d  7434  oveqan12d  7435  ovmpot  7577  mptmpoopabovd  8086  suppofssd  8206  sprmpod  8227  oev2  8517  oa00  8553  omopthi  8656  ecopoveq  8825  ecopovtrn  8827  isfsupp  9342  cantnffval  9649  ttrcltr  9702  fpwwe2lem4  10668  fpwwe2  10677  pwfseqlem4  10696  halfnq  11010  distrlem5pr  11061  addcmpblnr  11103  ltsrpr  11111  mulgt0sr  11139  add20  11775  msqge0  11784  recextlem2  11894  cru  12259  zaddcl  12683  qaddcl  13040  qmulcl  13042  xaddval  13300  xmulval  13302  xnn0xadd0  13324  xadddilem  13371  fzopth  13641  fzoopth  13843  modval  13957  1exp  14180  m1expeven  14198  nn0opthi  14359  faclbnd  14379  faclbnd3  14381  bcn0  14399  ccatopth  14810  ccatopth2  14811  repswccat  14882  reval  15218  absval  15350  clim  15606  rlim  15607  fsumparts  15918  cpnnen  16342  dvds2add  16405  dvds2sub  16406  opoe  16478  omoe  16479  opeo  16480  omeo  16481  gcddvds  16618  gcdcl  16621  gcdeq0  16632  gcdneg  16637  gcdaddmlem  16639  bezoutlem3  16656  bezout  16658  gcddiv  16666  nn0rppwr  16676  eucalgval2  16696  lcmabs  16720  rpmul  16774  divgcdcoprmex  16781  isprm5  16823  prmexpb  16835  rpexp  16838  nn0gcdsq  16868  pcqmul  16970  prmreclem3  17035  mul4sq  17071  vdwapval  17090  f1ocpbl  17636  homfval  17805  comfval  17813  issect  17867  isfull  18026  isfth  18030  natfval  18063  catchom  18217  catcco  18219  funcsetcestrclem5  18272  plusfval  18762  0subm  18952  cycsubm  19356  cyccom  19357  isgim  19415  subgga  19453  cayleylem1  19565  lsmsubm  19806  subgdisjb  19846  pj1fval  19847  odadd1  20001  qusabl  20018  imasabl  20029  dprdsubg  20179  rnghmval  20609  isrngim  20614  dfrhm2  20643  rhmval0  20644  isrhm  20648  isrim0  20652  crngrhmfo  20665  rhmval  20677  funcrngcsetcALT  20832  srhmsubclem3  20870  srhmsubc  20871  fldhmsubc  20981  scafval  21095  rmodislmodlem  21143  rmodislmod  21144  lss1d  21177  islmhm  21241  islmim  21276  prmidlc  21568  pzriprnglem5  21730  pzriprnglem8  21733  znfld  21805  cygznlem3  21814  cnmsgnsubg  21822  psgnghm  21825  ipeq0  21883  ipfval  21894  dsmmval  21979  dsmmacl  21986  mplval  22235  mplcoe5lem  22287  opsrval  22294  evlval  22348  mpfind  22363  selvffval  22366  mhpfval  22398  mhpmulcl  22409  psdffval  22417  mat1dimcrng  22731  dmatval  22746  dmatmulcl  22754  scmatval  22758  scmataddcl  22770  scmatsubcl  22771  scmatmulcl  22772  mavmul0g  22807  marrepfval  22814  marrepeval  22817  marepvfval  22819  marepveval  22822  submafval  22833  submaeval  22836  mdetfval  22840  madugsum  22897  minmar1fval  22900  minmar1eval  22903  symgmatr01  22908  gsummatr01lem3  22911  gsummatr01lem4  22912  gsummatr01  22913  cpmatacl  22973  mat2pmatfval  22980  mat2pmatvalel  22982  mat2pmatmul  22988  cpm2mfval  23006  cpm2mvalel  23008  m2cpminvid  23010  m2cpminvid2  23012  decpmate  23023  pmatcollpw1  23033  monmatcollpw  23036  pmatcollpwlem  23037  pmatcollpw  23038  pmatcollpwscmatlem2  23047  pm2mpval  23052  pm2mpf1  23056  mp2pm2mplem3  23065  mp2pm2mplem4  23066  chpmatfval  23087  tx2ndc  23909  cnmpt2t  23931  cnmpt22f  23933  hmeofval  24016  qustgplem  24379  stdbdmetval  24772  nmofval  24972  nghmfval  24980  isnmhm  25004  xrsxmet  25068  divcn  25128  divccn  25133  iihalf1cn  25192  iihalf2cn  25194  icchmeo  25201  cnrehmeo  25213  isphtpy  25241  isphtpc  25254  reparphti  25257  pcorevlem  25286  cphnm  25453  tcphnmval  25489  ipcau2  25494  tcphcphlem1  25495  tcphcphlem2  25496  tcphcph  25497  bcthlem1  25584  bcth  25589  mulcncf  25706  dyadmax  25858  volcn  25866  vitalilem1  25868  vitalilem2  25869  vitalilem3  25870  vitali  25873  i1fmullem  25954  itg1addlem4  25959  dvlip  26252  ftc1a  26296  mdegfval  26319  r1pval  26415  coeaddlem  26507  plycn  26519  quotval  26554  elqaalem2  26584  taylfval  26627  psercn2  26691  cxpcn  27014  cxpcn3  27017  resqrtcn  27018  sqrtcn  27019  abscxpbnd  27022  angval  27070  chordthmlem  27101  dcubic  27115  efrlim  27238  lgsdchr  27623  mul2sq  27687  ostthlem2  27896  zaddscl  28691  zmulscld  28694  zseo  28719  z12addscl  28774  tglngval  28925  islnopp  29126  ishpg  29148  elplngid  29171  lnincplng  29173  plngcp  29175  plngrot  29179  nhpmirhp  29187  lnperpexs  29221  ragraghl  29257  tgaaddcpbllem2  29261  tgaaddcpbl2  29264  angmgmaddeu1  29290  prlnghpg  29335  prlngmo  29343  finsumvtxdg2size  30042  wspthsn  30348  wwlksnon  30351  wspthsnon  30352  iswspthsnon  30356  2clwwlk  30859  numclwlk1lem2  30882  numclwwlkovh0  30884  hmoval  31323  htth  31431  normval  31637  hlimi  31701  hsn0elch  31761  ocsh  31796  shscli  31830  shs00i  31963  chj00i  32000  riesz4i  32576  stm1addi  32758  stm1add3i  32760  superpos  32867  elrgspnlem2  33715  drnglring  33935  idlsrgmulrval  33952  splyval  34102  brfinext  34195  finextfldext  34207  irngval  34228  minplyval  34248  submateq  34352  metidv  34435  rmulccn  34471  pl1cn  34498  sibfof  34884  cxpcncf1  35136  subfacval2  35849  txsconnlem  35902  cvxpconn  35904  cvxsconn  35905  iscvm  35921  prv  36090  mpomulnzcnf  36986  knoppcnlem10  37266  bj-bary1  38129  ismblfin  38475  itg2addnclem3  38487  itg2addnc  38488  ftc1anclem3  38509  ftc1anc  38515  bfp  38639  rngo2  38722  rngohomco  38789  rngoisoval  38792  rngoisocnv  38796  crngohomfo  38821  keridl  38847  ispridlc  38885  snatpsubN  40688  cdlemn11pre  42148  dihord2pre  42163  baerlem3lem1  42645  prjcrvfval  43542  mendval  44085  mendplusg  44088  omcl3g  44240  mulvval  45355  fprodcnlem  46494  climf  46517  climf2  46559  cxpcncf2  46792  smflimlem3  47666  fmtnofac2lem  48536  prmdvdsfmtnof1lem2  48553  opoeALTV  48664  opeoALTV  48665  rngchomALTV  49248  funcringcsetcALTV2lem5  49274  ringchomALTV  49282  funcringcsetclem5ALTV  49297  srhmsubcALTVlem2  49304  srhmsubcALTV  49305  fldhmsubcALTV  49313  dmatALTval  49395  lincsumcl  49426  fdivval  49534  catprslem  50001  catprsc  50004  catprsc2  50005  oppcendc  50009  thincmoALT  50420  functhinclem2  50436  fullthinc2  50442  setc1onsubc  50593  lmdfval  50640  cmdfval  50641  crosspdot0lem  50861