Theorem oveq12 7366

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  (class class class)co 7357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7360

This theorem is referenced by:  oveq12i  7369  oveq12d  7375  oveqan12d  7376  mptmpoopabovd  8014  mptmpoopabovdOLD  8016  suppofssd  8134  sprmpod  8155  oev2  8469  oa00  8506  omopthi  8607  ecopoveq  8757  ecopovtrn  8759  isfsupp  9309  cantnffval  9599  ttrcltr  9652  fpwwe2  10579  halfnq  10912  distrlem5pr  10963  addcmpblnr  11005  ltsrpr  11013  mulgt0sr  11041  add20  11667  msqge0  11676  recextlem2  11786  cru  12145  zaddcl  12543  qaddcl  12890  qmulcl  12892  xaddval  13142  xmulval  13144  xnn0xadd0  13166  xadddilem  13213  fzopth  13478  modval  13776  1exp  13997  m1expeven  14015  nn0opthi  14170  faclbnd  14190  faclbnd3  14192  bcn0  14210  ccatopth  14604  ccatopth2  14605  repswccat  14674  reval  14991  absval  15123  clim  15376  rlim  15377  fsumparts  15691  cpnnen  16111  dvds2add  16172  dvds2sub  16173  opoe  16245  omoe  16246  opeo  16247  omeo  16248  gcddvds  16383  gcdcl  16386  gcdeq0  16397  gcdneg  16402  gcdaddmlem  16404  gcdabsOLD  16412  bezoutlem3  16422  bezout  16424  gcddiv  16432  eucalgval2  16457  lcmabs  16481  rpmul  16535  divgcdcoprmex  16542  isprm5  16583  prmexpb  16596  rpexp  16598  nn0gcdsq  16627  pcqmul  16725  prmreclem3  16790  mul4sq  16826  vdwapval  16845  f1ocpbl  17407  homfval  17572  comfval  17580  issect  17636  isfull  17797  isfth  17801  natfval  17833  catchom  17989  catcco  17991  funcsetcestrclem5  18047  plusfval  18504  0subm  18628  cycsubm  18995  cyccom  18996  isgim  19052  subgga  19080  cayleylem1  19194  lsmsubm  19435  subgdisjb  19475  pj1fval  19476  odadd1  19626  qusabl  19643  dprdsubg  19803  dfrhm2  20148  isrhm  20152  isrim0OLD  20154  isrim0  20156  scafval  20341  rmodislmodlem  20389  rmodislmod  20390  rmodislmodOLD  20391  lss1d  20424  islmhm  20488  islmim  20523  znfld  20967  cygznlem3  20976  cnmsgnsubg  20981  psgnghm  20984  ipeq0  21042  ipfval  21053  dsmmval  21140  dsmmacl  21147  mplval  21397  mplcoe5lem  21440  opsrval  21447  evlval  21505  mpfind  21517  selvffval  21526  mhpfval  21529  mhpmulcl  21539  mat1dimcrng  21826  dmatval  21841  dmatmulcl  21849  scmatval  21853  scmataddcl  21865  scmatsubcl  21866  scmatmulcl  21867  mavmul0g  21902  marrepfval  21909  marrepeval  21912  marepvfval  21914  marepveval  21917  submafval  21928  submaeval  21931  mdetfval  21935  madugsum  21992  minmar1fval  21995  minmar1eval  21998  symgmatr01  22003  gsummatr01lem3  22006  gsummatr01lem4  22007  gsummatr01  22008  cpmatacl  22065  mat2pmatfval  22072  mat2pmatvalel  22074  mat2pmatmul  22080  cpm2mfval  22098  cpm2mvalel  22100  m2cpminvid  22102  m2cpminvid2  22104  decpmate  22115  pmatcollpw1  22125  monmatcollpw  22128  pmatcollpwlem  22129  pmatcollpw  22130  pmatcollpwscmatlem2  22139  pm2mpval  22144  pm2mpf1  22148  mp2pm2mplem3  22157  mp2pm2mplem4  22158  chpmatfval  22179  tx2ndc  23002  cnmpt2t  23024  cnmpt22f  23026  hmeofval  23109  qustgplem  23472  stdbdmetval  23870  nmofval  24078  nghmfval  24086  isnmhm  24110  xrsxmet  24172  isphtpy  24344  isphtpc  24357  pcorevlem  24389  cphnm  24557  tcphnmval  24593  ipcau2  24598  tcphcphlem1  24599  tcphcphlem2  24600  tcphcph  24601  bcthlem1  24688  bcth  24693  dyadmax  24962  volcn  24970  vitalilem1  24972  vitalilem2  24973  vitalilem3  24974  vitali  24977  i1fmullem  25058  itg1addlem4  25063  itg1addlem4OLD  25064  dvlip  25357  ftc1a  25401  mdegfval  25427  r1pval  25521  coeaddlem  25610  quotval  25652  elqaalem2  25680  taylfval  25718  cxpcn3  26101  resqrtcn  26102  sqrtcn  26103  abscxpbnd  26106  angval  26151  chordthmlem  26182  dcubic  26196  lgsdchr  26703  mul2sq  26767  ostthlem2  26976  tglngval  27493  islnopp  27681  ishpg  27701  finsumvtxdg2size  28498  wspthsn  28793  wwlksnon  28796  wspthsnon  28797  iswspthsnon  28801  2clwwlk  29291  numclwlk1lem2  29314  numclwwlkovh0  29316  hmoval  29752  htth  29860  normval  30066  hlimi  30130  hsn0elch  30190  ocsh  30225  shscli  30259  shs00i  30392  chj00i  30429  riesz4i  31005  stm1addi  31187  stm1add3i  31189  superpos  31296  prmidlc  32221  idlsrgmulrval  32251  brfinext  32342  irngval  32359  minplyval  32372  submateq  32390  metidv  32473  rmulccn  32509  pl1cn  32536  sibfof  32940  cxpcncf1  33208  subfacval2  33781  txsconnlem  33834  iscvm  33853  prv  34022  bj-bary1  35783  ismblfin  36119  itg2addnclem3  36131  itg2addnc  36132  ftc1anclem3  36153  ftc1anc  36159  bfp  36283  rngo2  36366  rngohomco  36433  rngoisoval  36436  rngoisocnv  36440  crngohomfo  36465  keridl  36491  ispridlc  36529  snatpsubN  38213  cdlemn11pre  39673  dihord2pre  39688  baerlem3lem1  40170  nn0rppwr  40805  sn-inelr  40920  prjcrvfval  40955  mendval  41496  mendplusg  41499  omcl3g  41653  mulvval  42738  climf  43853  climf2  43897  cxpcncf2  44130  smflimlem3  45004  fzoopth  45549  fmtnofac2lem  45750  prmdvdsfmtnof1lem2  45767  opoeALTV  45865  opeoALTV  45866  rnghmval  46179  isrngisom  46184  rhmval  46207  rngchomALTV  46273  funcrngcsetcALT  46287  funcringcsetcALTV2lem5  46328  ringchomALTV  46336  funcringcsetclem5ALTV  46351  srhmsubclem3  46363  srhmsubc  46364  fldhmsubc  46372  srhmsubcALTVlem2  46381  srhmsubcALTV  46382  fldhmsubcALTV  46390  dmatALTval  46471  lincsumcl  46502  fdivval  46615  catprslem  47020  catprsc  47023  catprsc2  47024  thincmoALT  47040  functhinclem2  47052  fullthinc2  47057