Theorem oveq12 7432

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

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

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426

This theorem is used by:  oveq12i  7435  oveq12d  7441  oveqan12d  7442  ovmpot  7584  mptmpoopabovd  8088  suppofssd  8208  sprmpod  8229  oev2  8517  oa00  8553  omopthi  8656  ecopoveq  8825  ecopovtrn  8827  isfsupp  9335  cantnffval  9642  ttrcltr  9695  fpwwe2lem4  10637  fpwwe2  10646  pwfseqlem4  10665  halfnq  10979  distrlem5pr  11030  addcmpblnr  11072  ltsrpr  11080  mulgt0sr  11108  add20  11744  msqge0  11753  recextlem2  11863  cru  12228  zaddcl  12652  qaddcl  13007  qmulcl  13009  xaddval  13267  xmulval  13269  xnn0xadd0  13291  xadddilem  13338  fzopth  13608  fzoopth  13810  modval  13924  1exp  14147  m1expeven  14165  nn0opthi  14326  faclbnd  14346  faclbnd3  14348  bcn0  14366  ccatopth  14777  ccatopth2  14778  repswccat  14849  reval  15183  absval  15315  clim  15571  rlim  15572  fsumparts  15884  cpnnen  16310  dvds2add  16373  dvds2sub  16374  opoe  16446  omoe  16447  opeo  16448  omeo  16449  gcddvds  16586  gcdcl  16589  gcdeq0  16600  gcdneg  16605  gcdaddmlem  16607  bezoutlem3  16624  bezout  16626  gcddiv  16634  nn0rppwr  16644  eucalgval2  16664  lcmabs  16688  rpmul  16742  divgcdcoprmex  16749  isprm5  16791  prmexpb  16803  rpexp  16806  nn0gcdsq  16836  pcqmul  16938  prmreclem3  17003  mul4sq  17039  vdwapval  17058  f1ocpbl  17604  homfval  17773  comfval  17781  issect  17835  isfull  17994  isfth  17998  natfval  18031  catchom  18185  catcco  18187  funcsetcestrclem5  18240  plusfval  18730  0subm  18901  cycsubm  19298  cyccom  19299  isgim  19357  subgga  19395  cayleylem1  19507  lsmsubm  19748  subgdisjb  19788  pj1fval  19789  odadd1  19943  qusabl  19960  imasabl  19971  dprdsubg  20121  rnghmval  20548  isrngim  20553  dfrhm2  20582  rhmval0  20583  isrhm  20587  isrim0  20591  crngrhmfo  20604  rhmval  20616  funcrngcsetcALT  20770  srhmsubclem3  20808  srhmsubc  20809  fldhmsubc  20918  scafval  21032  rmodislmodlem  21080  rmodislmod  21081  lss1d  21114  islmhm  21178  islmim  21213  prmidlc  21503  pzriprnglem5  21665  pzriprnglem8  21668  znfld  21740  cygznlem3  21749  cnmsgnsubg  21757  psgnghm  21760  ipeq0  21818  ipfval  21829  dsmmval  21914  dsmmacl  21921  mplval  22168  mplcoe5lem  22220  opsrval  22227  evlval  22281  mpfind  22296  selvffval  22299  mhpfval  22331  mhpmulcl  22342  psdffval  22350  mat1dimcrng  22664  dmatval  22679  dmatmulcl  22687  scmatval  22691  scmataddcl  22703  scmatsubcl  22704  scmatmulcl  22705  mavmul0g  22740  marrepfval  22747  marrepeval  22750  marepvfval  22752  marepveval  22755  submafval  22766  submaeval  22769  mdetfval  22773  madugsum  22830  minmar1fval  22833  minmar1eval  22836  symgmatr01  22841  gsummatr01lem3  22844  gsummatr01lem4  22845  gsummatr01  22846  cpmatacl  22903  mat2pmatfval  22910  mat2pmatvalel  22912  mat2pmatmul  22918  cpm2mfval  22936  cpm2mvalel  22938  m2cpminvid  22940  m2cpminvid2  22942  decpmate  22953  pmatcollpw1  22963  monmatcollpw  22966  pmatcollpwlem  22967  pmatcollpw  22968  pmatcollpwscmatlem2  22977  pm2mpval  22982  pm2mpf1  22986  mp2pm2mplem3  22995  mp2pm2mplem4  22996  chpmatfval  23017  tx2ndc  23838  cnmpt2t  23860  cnmpt22f  23862  hmeofval  23945  qustgplem  24308  stdbdmetval  24701  nmofval  24901  nghmfval  24909  isnmhm  24933  xrsxmet  24997  divcn  25057  divccn  25062  iihalf1cn  25121  iihalf2cn  25123  icchmeo  25130  cnrehmeo  25142  isphtpy  25170  isphtpc  25183  reparphti  25186  pcorevlem  25215  cphnm  25382  tcphnmval  25418  ipcau2  25423  tcphcphlem1  25424  tcphcphlem2  25425  tcphcph  25426  bcthlem1  25513  bcth  25518  mulcncf  25635  dyadmax  25787  volcn  25795  vitalilem1  25797  vitalilem2  25798  vitalilem3  25799  vitali  25802  i1fmullem  25883  itg1addlem4  25888  dvlip  26182  ftc1a  26226  mdegfval  26249  r1pval  26345  coeaddlem  26436  plycn  26448  quotval  26483  elqaalem2  26511  taylfval  26552  psercn2  26616  cxpcn  26940  cxpcn3  26943  resqrtcn  26944  sqrtcn  26945  abscxpbnd  26948  angval  26996  chordthmlem  27027  dcubic  27041  efrlim  27164  lgsdchr  27549  mul2sq  27613  ostthlem2  27822  zaddscl  28617  zmulscld  28620  zseo  28645  z12addscl  28700  tglngval  28850  islnopp  29050  ishpg  29071  elplngid  29094  lnincplng  29096  plngcp  29098  plngrot  29102  nhpmirhp  29110  lnperpexs  29144  ragraghl  29179  prlnghpg  29226  prlngmo  29234  finsumvtxdg2size  29930  wspthsn  30227  wwlksnon  30230  wspthsnon  30231  iswspthsnon  30235  2clwwlk  30728  numclwlk1lem2  30751  numclwwlkovh0  30753  hmoval  31192  htth  31300  normval  31506  hlimi  31570  hsn0elch  31630  ocsh  31665  shscli  31699  shs00i  31832  chj00i  31869  riesz4i  32445  stm1addi  32627  stm1add3i  32629  superpos  32736  elrgspnlem2  33587  drnglring  33806  idlsrgmulrval  33823  splyval  33973  brfinext  34066  finextfldext  34078  irngval  34099  minplyval  34119  submateq  34223  metidv  34306  rmulccn  34342  pl1cn  34369  sibfof  34754  cxpcncf1  35006  subfacval2  35692  txsconnlem  35745  cvxpconn  35747  cvxsconn  35748  iscvm  35764  prv  35933  mpomulnzcnf  36844  knoppcnlem10  37124  bj-bary1  37989  ismblfin  38345  itg2addnclem3  38357  itg2addnc  38358  ftc1anclem3  38379  ftc1anc  38385  bfp  38508  rngo2  38591  rngohomco  38658  rngoisoval  38661  rngoisocnv  38665  crngohomfo  38690  keridl  38716  ispridlc  38754  snatpsubN  40557  cdlemn11pre  42017  dihord2pre  42032  baerlem3lem1  42514  prjcrvfval  43396  mendval  43939  mendplusg  43942  omcl3g  44094  mulvval  45209  fprodcnlem  46348  climf  46371  climf2  46413  cxpcncf2  46646  smflimlem3  47520  fmtnofac2lem  48353  prmdvdsfmtnof1lem2  48370  opoeALTV  48481  opeoALTV  48482  rngchomALTV  49066  funcringcsetcALTV2lem5  49092  ringchomALTV  49100  funcringcsetclem5ALTV  49115  srhmsubcALTVlem2  49122  srhmsubcALTV  49123  fldhmsubcALTV  49131  dmatALTval  49213  lincsumcl  49244  fdivval  49352  catprslem  49821  catprsc  49824  catprsc2  49825  oppcendc  49829  thincmoALT  50240  functhinclem2  50256  fullthinc2  50262  setc1onsubc  50413  lmdfval  50460  cmdfval  50461