Theorem oveq12 7376

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  (class class class)co 7367

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  oveq12i  7379  oveq12d  7385  oveqan12d  7386  ovmpot  7528  mptmpoopabovd  8034  suppofssd  8153  sprmpod  8174  oev2  8458  oa00  8494  omopthi  8597  ecopoveq  8765  ecopovtrn  8767  isfsupp  9278  cantnffval  9584  ttrcltr  9637  fpwwe2lem4  10557  fpwwe2  10566  pwfseqlem4  10585  halfnq  10899  distrlem5pr  10950  addcmpblnr  10992  ltsrpr  11000  mulgt0sr  11028  add20  11662  msqge0  11671  recextlem2  11781  cru  12151  zaddcl  12567  qaddcl  12915  qmulcl  12917  xaddval  13175  xmulval  13177  xnn0xadd0  13199  xadddilem  13246  fzopth  13515  fzoopth  13717  modval  13830  1exp  14053  m1expeven  14071  nn0opthi  14232  faclbnd  14252  faclbnd3  14254  bcn0  14272  ccatopth  14678  ccatopth2  14679  repswccat  14748  reval  15068  absval  15200  clim  15456  rlim  15457  fsumparts  15769  cpnnen  16196  dvds2add  16259  dvds2sub  16260  opoe  16332  omoe  16333  opeo  16334  omeo  16335  gcddvds  16472  gcdcl  16475  gcdeq0  16486  gcdneg  16491  gcdaddmlem  16493  bezoutlem3  16510  bezout  16512  gcddiv  16520  nn0rppwr  16530  eucalgval2  16550  lcmabs  16574  rpmul  16628  divgcdcoprmex  16635  isprm5  16677  prmexpb  16689  rpexp  16692  nn0gcdsq  16722  pcqmul  16824  prmreclem3  16889  mul4sq  16925  vdwapval  16944  f1ocpbl  17489  homfval  17658  comfval  17666  issect  17720  isfull  17879  isfth  17883  natfval  17916  catchom  18070  catcco  18072  funcsetcestrclem5  18125  plusfval  18615  0subm  18785  cycsubm  19177  cyccom  19178  isgim  19237  subgga  19275  cayleylem1  19387  lsmsubm  19628  subgdisjb  19668  pj1fval  19669  odadd1  19823  qusabl  19840  imasabl  19851  dprdsubg  20001  rnghmval  20420  isrngim  20425  dfrhm2  20454  isrhm  20458  isrim0  20462  rhmval  20477  funcrngcsetcALT  20618  srhmsubclem3  20656  srhmsubc  20657  fldhmsubc  20762  scafval  20876  rmodislmodlem  20924  rmodislmod  20925  lss1d  20958  islmhm  21022  islmim  21057  pzriprnglem5  21465  pzriprnglem8  21468  znfld  21540  cygznlem3  21549  cnmsgnsubg  21557  psgnghm  21560  ipeq0  21618  ipfval  21629  dsmmval  21714  dsmmacl  21721  mplval  21967  mplcoe5lem  22017  opsrval  22024  evlval  22078  mpfind  22093  selvffval  22099  mhpfval  22104  mhpmulcl  22115  psdffval  22123  mat1dimcrng  22442  dmatval  22457  dmatmulcl  22465  scmatval  22469  scmataddcl  22481  scmatsubcl  22482  scmatmulcl  22483  mavmul0g  22518  marrepfval  22525  marrepeval  22528  marepvfval  22530  marepveval  22533  submafval  22544  submaeval  22547  mdetfval  22551  madugsum  22608  minmar1fval  22611  minmar1eval  22614  symgmatr01  22619  gsummatr01lem3  22622  gsummatr01lem4  22623  gsummatr01  22624  cpmatacl  22681  mat2pmatfval  22688  mat2pmatvalel  22690  mat2pmatmul  22696  cpm2mfval  22714  cpm2mvalel  22716  m2cpminvid  22718  m2cpminvid2  22720  decpmate  22731  pmatcollpw1  22741  monmatcollpw  22744  pmatcollpwlem  22745  pmatcollpw  22746  pmatcollpwscmatlem2  22755  pm2mpval  22760  pm2mpf1  22764  mp2pm2mplem3  22773  mp2pm2mplem4  22774  chpmatfval  22795  tx2ndc  23616  cnmpt2t  23638  cnmpt22f  23640  hmeofval  23723  qustgplem  24086  stdbdmetval  24479  nmofval  24679  nghmfval  24687  isnmhm  24711  xrsxmet  24775  divcn  24835  divccn  24840  iihalf1cn  24899  iihalf2cn  24901  icchmeo  24908  cnrehmeo  24920  isphtpy  24948  isphtpc  24961  reparphti  24964  pcorevlem  24993  cphnm  25160  tcphnmval  25196  ipcau2  25201  tcphcphlem1  25202  tcphcphlem2  25203  tcphcph  25204  bcthlem1  25291  bcth  25296  mulcncf  25413  dyadmax  25565  volcn  25573  vitalilem1  25575  vitalilem2  25576  vitalilem3  25577  vitali  25580  i1fmullem  25661  itg1addlem4  25666  dvlip  25960  ftc1a  26004  mdegfval  26027  r1pval  26123  coeaddlem  26214  plycn  26226  quotval  26258  elqaalem2  26286  taylfval  26324  psercn2  26388  cxpcn  26709  cxpcn3  26712  resqrtcn  26713  sqrtcn  26714  abscxpbnd  26717  angval  26765  chordthmlem  26796  dcubic  26810  efrlim  26933  lgsdchr  27318  mul2sq  27382  ostthlem2  27591  zaddscl  28386  zmulscld  28389  zseo  28414  z12addscl  28469  tglngval  28619  islnopp  28807  ishpg  28827  finsumvtxdg2size  29619  wspthsn  29916  wwlksnon  29919  wspthsnon  29920  iswspthsnon  29924  2clwwlk  30417  numclwlk1lem2  30440  numclwwlkovh0  30442  hmoval  30881  htth  30989  normval  31195  hlimi  31259  hsn0elch  31319  ocsh  31354  shscli  31388  shs00i  31521  chj00i  31558  riesz4i  32134  stm1addi  32316  stm1add3i  32318  superpos  32425  elrgspnlem2  33304  prmidlc  33508  idlsrgmulrval  33569  splyval  33703  brfinext  33796  finextfldext  33808  irngval  33829  minplyval  33849  submateq  33953  metidv  34036  rmulccn  34072  pl1cn  34099  sibfof  34484  cxpcncf1  34739  subfacval2  35369  txsconnlem  35422  cvxpconn  35424  cvxsconn  35425  iscvm  35441  prv  35610  mpomulnzcnf  36481  knoppcnlem10  36762  bj-bary1  37626  ismblfin  37982  itg2addnclem3  37994  itg2addnc  37995  ftc1anclem3  38016  ftc1anc  38022  bfp  38145  rngo2  38228  rngohomco  38295  rngoisoval  38298  rngoisocnv  38302  crngohomfo  38327  keridl  38353  ispridlc  38391  snatpsubN  40196  cdlemn11pre  41656  dihord2pre  41671  baerlem3lem1  42153  prjcrvfval  43064  mendval  43607  mendplusg  43610  omcl3g  43762  mulvval  44894  fprodcnlem  46029  climf  46052  climf2  46094  cxpcncf2  46327  smflimlem3  47201  fmtnofac2lem  48031  prmdvdsfmtnof1lem2  48048  opoeALTV  48159  opeoALTV  48160  rngchomALTV  48744  funcringcsetcALTV2lem5  48770  ringchomALTV  48778  funcringcsetclem5ALTV  48793  srhmsubcALTVlem2  48800  srhmsubcALTV  48801  fldhmsubcALTV  48809  dmatALTval  48876  lincsumcl  48907  fdivval  49015  catprslem  49485  catprsc  49488  catprsc2  49489  oppcendc  49493  thincmoALT  49904  functhinclem2  49920  fullthinc2  49926  setc1onsubc  50077  lmdfval  50124  cmdfval  50125