Theorem oveq12 7369

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548  (class class class)co 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-iota 6445  df-fv 6497  df-ov 7363

This theorem is referenced by:  oveq12i  7372  oveq12d  7378  oveqan12d  7379  ovmpot  7521  mptmpoopabovd  8027  suppofssd  8147  sprmpod  8168  oev2  8452  oa00  8488  omopthi  8591  ecopoveq  8759  ecopovtrn  8761  isfsupp  9272  cantnffval  9579  ttrcltr  9632  fpwwe2lem4  10552  fpwwe2  10561  pwfseqlem4  10580  halfnq  10894  distrlem5pr  10945  addcmpblnr  10987  ltsrpr  10995  mulgt0sr  11023  add20  11657  msqge0  11666  recextlem2  11776  cru  12146  zaddcl  12562  qaddcl  12910  qmulcl  12912  xaddval  13170  xmulval  13172  xnn0xadd0  13194  xadddilem  13241  fzopth  13510  fzoopth  13712  modval  13825  1exp  14048  m1expeven  14066  nn0opthi  14227  faclbnd  14247  faclbnd3  14249  bcn0  14267  ccatopth  14673  ccatopth2  14674  repswccat  14743  reval  15063  absval  15195  clim  15451  rlim  15452  fsumparts  15764  cpnnen  16191  dvds2add  16254  dvds2sub  16255  opoe  16327  omoe  16328  opeo  16329  omeo  16330  gcddvds  16467  gcdcl  16470  gcdeq0  16481  gcdneg  16486  gcdaddmlem  16488  bezoutlem3  16505  bezout  16507  gcddiv  16515  nn0rppwr  16525  eucalgval2  16545  lcmabs  16569  rpmul  16623  divgcdcoprmex  16630  isprm5  16672  prmexpb  16684  rpexp  16687  nn0gcdsq  16717  pcqmul  16819  prmreclem3  16884  mul4sq  16920  vdwapval  16939  f1ocpbl  17484  homfval  17653  comfval  17661  issect  17715  isfull  17874  isfth  17878  natfval  17911  catchom  18065  catcco  18067  funcsetcestrclem5  18120  plusfval  18610  0subm  18780  cycsubm  19172  cyccom  19173  isgim  19232  subgga  19270  cayleylem1  19382  lsmsubm  19623  subgdisjb  19663  pj1fval  19664  odadd1  19818  qusabl  19835  imasabl  19846  dprdsubg  19996  rnghmval  20415  isrngim  20420  dfrhm2  20449  isrhm  20453  isrim0  20457  rhmval  20475  funcrngcsetcALT  20617  srhmsubclem3  20655  srhmsubc  20656  fldhmsubc  20761  scafval  20875  rmodislmodlem  20923  rmodislmod  20924  lss1d  20957  islmhm  21021  islmim  21056  pzriprnglem5  21464  pzriprnglem8  21467  znfld  21539  cygznlem3  21548  cnmsgnsubg  21556  psgnghm  21559  ipeq0  21617  ipfval  21628  dsmmval  21713  dsmmacl  21720  mplval  21967  mplcoe5lem  22019  opsrval  22026  evlval  22080  mpfind  22095  selvffval  22098  mhpfval  22130  mhpmulcl  22141  psdffval  22149  mat1dimcrng  22464  dmatval  22479  dmatmulcl  22487  scmatval  22491  scmataddcl  22503  scmatsubcl  22504  scmatmulcl  22505  mavmul0g  22540  marrepfval  22547  marrepeval  22550  marepvfval  22552  marepveval  22555  submafval  22566  submaeval  22569  mdetfval  22573  madugsum  22630  minmar1fval  22633  minmar1eval  22636  symgmatr01  22641  gsummatr01lem3  22644  gsummatr01lem4  22645  gsummatr01  22646  cpmatacl  22703  mat2pmatfval  22710  mat2pmatvalel  22712  mat2pmatmul  22718  cpm2mfval  22736  cpm2mvalel  22738  m2cpminvid  22740  m2cpminvid2  22742  decpmate  22753  pmatcollpw1  22763  monmatcollpw  22766  pmatcollpwlem  22767  pmatcollpw  22768  pmatcollpwscmatlem2  22777  pm2mpval  22782  pm2mpf1  22786  mp2pm2mplem3  22795  mp2pm2mplem4  22796  chpmatfval  22817  tx2ndc  23638  cnmpt2t  23660  cnmpt22f  23662  hmeofval  23745  qustgplem  24108  stdbdmetval  24501  nmofval  24701  nghmfval  24709  isnmhm  24733  xrsxmet  24797  divcn  24857  divccn  24862  iihalf1cn  24921  iihalf2cn  24923  icchmeo  24930  cnrehmeo  24942  isphtpy  24970  isphtpc  24983  reparphti  24986  pcorevlem  25015  cphnm  25182  tcphnmval  25218  ipcau2  25223  tcphcphlem1  25224  tcphcphlem2  25225  tcphcph  25226  bcthlem1  25313  bcth  25318  mulcncf  25435  dyadmax  25587  volcn  25595  vitalilem1  25597  vitalilem2  25598  vitalilem3  25599  vitali  25602  i1fmullem  25683  itg1addlem4  25688  dvlip  25982  ftc1a  26026  mdegfval  26049  r1pval  26145  coeaddlem  26236  plycn  26248  quotval  26280  elqaalem2  26308  taylfval  26346  psercn2  26410  cxpcn  26731  cxpcn3  26734  resqrtcn  26735  sqrtcn  26736  abscxpbnd  26739  angval  26787  chordthmlem  26818  dcubic  26832  efrlim  26955  lgsdchr  27340  mul2sq  27404  ostthlem2  27613  zaddscl  28408  zmulscld  28411  zseo  28436  z12addscl  28491  tglngval  28641  islnopp  28829  ishpg  28849  finsumvtxdg2size  29641  wspthsn  29938  wwlksnon  29941  wspthsnon  29942  iswspthsnon  29946  2clwwlk  30439  numclwlk1lem2  30462  numclwwlkovh0  30464  hmoval  30903  htth  31011  normval  31217  hlimi  31281  hsn0elch  31341  ocsh  31376  shscli  31410  shs00i  31543  chj00i  31580  riesz4i  32156  stm1addi  32338  stm1add3i  32340  superpos  32447  elrgspnlem2  33328  prmidlc  33535  drnglring  33587  idlsrgmulrval  33604  splyval  33755  brfinext  33848  finextfldext  33860  irngval  33881  minplyval  33901  submateq  34005  metidv  34088  rmulccn  34124  pl1cn  34151  sibfof  34536  cxpcncf1  34791  subfacval2  35430  txsconnlem  35483  cvxpconn  35485  cvxsconn  35486  iscvm  35502  prv  35671  mpomulnzcnf  36542  knoppcnlem10  36823  bj-bary1  37687  ismblfin  38043  itg2addnclem3  38055  itg2addnc  38056  ftc1anclem3  38077  ftc1anc  38083  bfp  38206  rngo2  38289  rngohomco  38356  rngoisoval  38359  rngoisocnv  38363  crngohomfo  38388  keridl  38414  ispridlc  38452  snatpsubN  40257  cdlemn11pre  41717  dihord2pre  41732  baerlem3lem1  42214  prjcrvfval  43096  mendval  43639  mendplusg  43642  omcl3g  43794  mulvval  44926  fprodcnlem  46058  climf  46081  climf2  46123  cxpcncf2  46356  smflimlem3  47230  fmtnofac2lem  48060  prmdvdsfmtnof1lem2  48077  opoeALTV  48188  opeoALTV  48189  rngchomALTV  48773  funcringcsetcALTV2lem5  48799  ringchomALTV  48807  funcringcsetclem5ALTV  48822  srhmsubcALTVlem2  48829  srhmsubcALTV  48830  fldhmsubcALTV  48838  dmatALTval  48905  lincsumcl  48936  fdivval  49044  catprslem  49514  catprsc  49517  catprsc2  49518  oppcendc  49522  thincmoALT  49933  functhinclem2  49949  fullthinc2  49955  setc1onsubc  50106  lmdfval  50153  cmdfval  50154