Theorem oveq12 7449

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6509  df-fv 6563  df-ov 7443

This theorem is used by:  oveq12i  7452  oveq12d  7458  oveqan12d  7459  ovmpot  7602  mptmpoopabovd  8117  suppofssd  8245  sprmpod  8266  oev2  8556  oa00  8592  omopthi  8695  ecopoveq  8864  ecopovtrn  8866  isfsupp  9382  cantnffval  9688  ttrcltr  9741  fpwwe2lem4  10743  fpwwe2  10752  pwfseqlem4  10771  halfnq  11085  distrlem5pr  11136  addcmpblnr  11178  ltsrpr  11186  mulgt0sr  11214  add20  11852  msqge0  11861  recextlem2  11971  cru  12336  zaddcl  12760  qaddcl  13117  qmulcl  13119  xaddval  13377  xmulval  13379  xnn0xadd0  13401  xadddilem  13448  fzopth  13719  fzoopth  13921  modval  14035  1exp  14258  m1expeven  14276  nn0opthi  14438  faclbnd  14458  faclbnd3  14460  bcn0  14478  ccatopth  14890  ccatopth2  14891  repswccat  14962  reval  15299  absval  15431  clim  15687  rlim  15688  fsumparts  15999  cpnnen  16423  dvds2add  16486  dvds2sub  16487  opoe  16559  omoe  16560  opeo  16561  omeo  16562  gcddvds  16699  gcdcl  16702  gcdeq0  16715  gcdneg  16720  gcdaddmlem  16722  bezoutlem3  16740  bezout  16742  gcddiv  16750  nn0rppwr  16761  eucalgval2  16782  lcmabs  16806  rpmul  16860  divgcdcoprmex  16867  isprm5  16909  prmexpb  16921  rpexp  16924  nn0gcdsq  16954  pcqmul  17057  prmreclem3  17122  mul4sq  17158  vdwapval  17177  f1ocpbl  17723  homfval  17892  comfval  17900  issect  17954  isfull  18113  isfth  18117  natfval  18150  catchom  18304  catcco  18306  funcsetcestrclem5  18359  plusfval  18849  0subm  19039  cycsubm  19443  cyccom  19444  isgim  19502  subgga  19541  cayleylem1  19653  lsmsubm  19894  subgdisjb  19934  pj1fval  19935  odadd1  20089  qusabl  20106  imasabl  20117  dprdsubg  20267  rnghmval  20697  isrngim  20702  dfrhm2  20731  rhmval0  20732  isrhm  20736  isrim0  20740  crngrhmfo  20753  rhmval  20765  funcrngcsetcALT  20920  srhmsubclem3  20958  srhmsubc  20959  fldhmsubc  21069  scafval  21183  rmodislmodlem  21231  rmodislmod  21232  lss1d  21265  islmhm  21329  islmim  21364  prmidlc  21656  pzriprnglem5  21818  pzriprnglem8  21821  znfld  21893  cygznlem3  21902  cnmsgnsubg  21910  psgnghm  21913  ipeq0  21971  ipfval  21982  dsmmval  22067  dsmmacl  22074  mplval  22323  mplcoe5lem  22375  opsrval  22382  evlval  22436  mpfind  22451  selvffval  22454  mhpfval  22486  mhpmulcl  22497  psdffval  22505  mat1dimcrng  22819  dmatval  22834  dmatmulcl  22842  scmatval  22846  scmataddcl  22858  scmatsubcl  22859  scmatmulcl  22860  mavmul0g  22895  marrepfval  22902  marrepeval  22905  marepvfval  22907  marepveval  22910  submafval  22921  submaeval  22924  mdetfval  22928  madugsum  22985  minmar1fval  22988  minmar1eval  22991  symgmatr01  22996  gsummatr01lem3  22999  gsummatr01lem4  23000  gsummatr01  23001  cpmatacl  23061  mat2pmatfval  23068  mat2pmatvalel  23070  mat2pmatmul  23076  cpm2mfval  23094  cpm2mvalel  23096  m2cpminvid  23098  m2cpminvid2  23100  decpmate  23111  pmatcollpw1  23121  monmatcollpw  23124  pmatcollpwlem  23125  pmatcollpw  23126  pmatcollpwscmatlem2  23135  pm2mpval  23140  pm2mpf1  23144  mp2pm2mplem3  23153  mp2pm2mplem4  23154  chpmatfval  23175  tx2ndc  23997  cnmpt2t  24019  cnmpt22f  24021  hmeofval  24104  qustgplem  24467  stdbdmetval  24860  nmofval  25060  nghmfval  25068  isnmhm  25092  xrsxmet  25156  divcn  25216  divccn  25221  iihalf1cn  25280  iihalf2cn  25282  icchmeo  25289  cnrehmeo  25301  isphtpy  25329  isphtpc  25342  reparphti  25345  pcorevlem  25374  cphnm  25541  tcphnmval  25577  ipcau2  25582  tcphcphlem1  25583  tcphcphlem2  25584  tcphcph  25585  bcthlem1  25672  bcth  25677  mulcncf  25794  dyadmax  25946  volcn  25954  vitalilem1  25956  vitalilem2  25957  vitalilem3  25958  vitali  25961  i1fmullem  26042  itg1addlem4  26047  dvlip  26340  ftc1a  26384  mdegfval  26407  r1pval  26503  coeaddlem  26595  plycn  26607  quotval  26640  elqaalem2  26670  taylfval  26713  psercn2  26777  cxpcn  27100  cxpcn3  27103  resqrtcn  27104  sqrtcn  27105  abscxpbnd  27108  angval  27156  chordthmlem  27187  dcubic  27201  efrlim  27324  lgsdchr  27709  mul2sq  27773  ostthlem2  27982  zaddscl  28807  zmulscld  28810  zseo  28835  z12addscl  28890  tglngval  29041  islnopp  29242  ishpg  29264  elplngid  29287  lnincplng  29289  plngcp  29291  plngrot  29295  nhpmirhp  29303  lnperpexs  29337  ragraghl  29373  tgaaddcpbllem2  29377  tgaaddcpbl2  29380  angmgmaddeu1  29406  prlnghpg  29451  prlngmo  29459  finsumvtxdg2size  30158  wspthsn  30464  wwlksnon  30467  wspthsnon  30468  iswspthsnon  30472  2clwwlk  30975  numclwlk1lem2  30998  numclwwlkovh0  31000  hmoval  31439  htth  31547  normval  31753  hlimi  31817  hsn0elch  31877  ocsh  31912  shscli  31946  shs00i  32079  chj00i  32116  riesz4i  32692  stm1addi  32874  stm1add3i  32876  superpos  32983  elrgspnlem2  33871  drnglring  34091  idlsrgmulrval  34108  splyval  34258  brfinext  34351  finextfldext  34363  irngval  34384  minplyval  34404  submateq  34508  metidv  34591  rmulccn  34627  pl1cn  34654  sibfof  35039  cxpcncf1  35291  subfacval2  36118  txsconnlem  36171  cvxpconn  36173  cvxsconn  36174  iscvm  36190  prv  36359  mpomulnzcnf  37265  knoppcnlem10  37545  bj-bary1  38424  ismblfin  38770  itg2addnclem3  38782  itg2addnc  38783  ftc1anclem3  38804  ftc1anc  38810  bfp  38949  rngo2  39032  rngohomco  39099  rngoisoval  39102  rngoisocnv  39106  crngohomfo  39131  keridl  39157  ispridlc  39195  snatpsubN  40998  cdlemn11pre  42458  dihord2pre  42473  baerlem3lem1  42955  prjcrvfval  43858  mendval  44371  mendplusg  44374  omcl3g  44526  mulvval  45639  fprodcnlem  46814  climf  46837  climf2  46879  cxpcncf2  47112  smflimlem3  47986  fmtnofac2lem  48856  prmdvdsfmtnof1lem2  48873  opoeALTV  48984  opeoALTV  48985  rngchomALTV  49568  funcringcsetcALTV2lem5  49594  ringchomALTV  49602  funcringcsetclem5ALTV  49617  srhmsubcALTVlem2  49624  srhmsubcALTV  49625  fldhmsubcALTV  49633  dmatALTval  49715  lincsumcl  49746  fdivval  49854  catprslem  50327  catprsc  50330  catprsc2  50331  oppcendc  50335  thincmoALT  50767  functhinclem2  50783  fullthinc2  50789  setc1onsubc  50943  lmdfval  51035  cmdfval  51036  crosspdot0lem  51241