Theorem oveq12 7420

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  oveq12i  7423  oveq12d  7429  oveqan12d  7430  ovmpot  7572  mptmpoopabovd  8079  suppofssd  8199  sprmpod  8220  oev2  8508  oa00  8544  omopthi  8647  ecopoveq  8816  ecopovtrn  8818  isfsupp  9325  cantnffval  9632  ttrcltr  9685  fpwwe2lem4  10619  fpwwe2  10628  pwfseqlem4  10647  halfnq  10961  distrlem5pr  11012  addcmpblnr  11054  ltsrpr  11062  mulgt0sr  11090  add20  11726  msqge0  11735  recextlem2  11845  cru  12210  zaddcl  12634  qaddcl  12989  qmulcl  12991  xaddval  13249  xmulval  13251  xnn0xadd0  13273  xadddilem  13320  fzopth  13589  fzoopth  13791  modval  13904  1exp  14127  m1expeven  14145  nn0opthi  14306  faclbnd  14326  faclbnd3  14328  bcn0  14346  ccatopth  14753  ccatopth2  14754  repswccat  14823  reval  15157  absval  15289  clim  15545  rlim  15546  fsumparts  15858  cpnnen  16285  dvds2add  16348  dvds2sub  16349  opoe  16421  omoe  16422  opeo  16423  omeo  16424  gcddvds  16561  gcdcl  16564  gcdeq0  16575  gcdneg  16580  gcdaddmlem  16582  bezoutlem3  16599  bezout  16601  gcddiv  16609  nn0rppwr  16619  eucalgval2  16639  lcmabs  16663  rpmul  16717  divgcdcoprmex  16724  isprm5  16766  prmexpb  16778  rpexp  16781  nn0gcdsq  16811  pcqmul  16913  prmreclem3  16978  mul4sq  17014  vdwapval  17033  f1ocpbl  17579  homfval  17748  comfval  17756  issect  17810  isfull  17969  isfth  17973  natfval  18006  catchom  18160  catcco  18162  funcsetcestrclem5  18215  plusfval  18705  0subm  18876  cycsubm  19273  cyccom  19274  isgim  19332  subgga  19370  cayleylem1  19482  lsmsubm  19723  subgdisjb  19763  pj1fval  19764  odadd1  19918  qusabl  19935  imasabl  19946  dprdsubg  20096  rnghmval  20522  isrngim  20527  dfrhm2  20556  isrhm  20560  isrim0  20564  rhmval  20582  funcrngcsetcALT  20726  srhmsubclem3  20764  srhmsubc  20765  fldhmsubc  20866  scafval  20980  rmodislmodlem  21028  rmodislmod  21029  lss1d  21062  islmhm  21126  islmim  21161  prmidlc  21444  pzriprnglem5  21604  pzriprnglem8  21607  znfld  21679  cygznlem3  21688  cnmsgnsubg  21696  psgnghm  21699  ipeq0  21757  ipfval  21768  dsmmval  21853  dsmmacl  21860  mplval  22107  mplcoe5lem  22159  opsrval  22166  evlval  22220  mpfind  22235  selvffval  22238  mhpfval  22270  mhpmulcl  22281  psdffval  22289  mat1dimcrng  22603  dmatval  22618  dmatmulcl  22626  scmatval  22630  scmataddcl  22642  scmatsubcl  22643  scmatmulcl  22644  mavmul0g  22679  marrepfval  22686  marrepeval  22689  marepvfval  22691  marepveval  22694  submafval  22705  submaeval  22708  mdetfval  22712  madugsum  22769  minmar1fval  22772  minmar1eval  22775  symgmatr01  22780  gsummatr01lem3  22783  gsummatr01lem4  22784  gsummatr01  22785  cpmatacl  22842  mat2pmatfval  22849  mat2pmatvalel  22851  mat2pmatmul  22857  cpm2mfval  22875  cpm2mvalel  22877  m2cpminvid  22879  m2cpminvid2  22881  decpmate  22892  pmatcollpw1  22902  monmatcollpw  22905  pmatcollpwlem  22906  pmatcollpw  22907  pmatcollpwscmatlem2  22916  pm2mpval  22921  pm2mpf1  22925  mp2pm2mplem3  22934  mp2pm2mplem4  22935  chpmatfval  22956  tx2ndc  23777  cnmpt2t  23799  cnmpt22f  23801  hmeofval  23884  qustgplem  24247  stdbdmetval  24640  nmofval  24840  nghmfval  24848  isnmhm  24872  xrsxmet  24936  divcn  24996  divccn  25001  iihalf1cn  25060  iihalf2cn  25062  icchmeo  25069  cnrehmeo  25081  isphtpy  25109  isphtpc  25122  reparphti  25125  pcorevlem  25154  cphnm  25321  tcphnmval  25357  ipcau2  25362  tcphcphlem1  25363  tcphcphlem2  25364  tcphcph  25365  bcthlem1  25452  bcth  25457  mulcncf  25574  dyadmax  25726  volcn  25734  vitalilem1  25736  vitalilem2  25737  vitalilem3  25738  vitali  25741  i1fmullem  25822  itg1addlem4  25827  dvlip  26121  ftc1a  26165  mdegfval  26188  r1pval  26284  coeaddlem  26375  plycn  26387  quotval  26422  elqaalem2  26450  taylfval  26488  psercn2  26552  cxpcn  26876  cxpcn3  26879  resqrtcn  26880  sqrtcn  26881  abscxpbnd  26884  angval  26932  chordthmlem  26963  dcubic  26977  efrlim  27100  lgsdchr  27485  mul2sq  27549  ostthlem2  27758  zaddscl  28553  zmulscld  28556  zseo  28581  z12addscl  28636  tglngval  28786  islnopp  28979  ishpg  29000  elplngid  29022  lnincplng  29024  plngcp  29026  plngrot  29030  nhpmirhp  29038  lnperpexs  29071  ragraghl  29104  prlnghpg  29151  prlngmo  29157  finsumvtxdg2size  29841  wspthsn  30138  wwlksnon  30141  wspthsnon  30142  iswspthsnon  30146  2clwwlk  30639  numclwlk1lem2  30662  numclwwlkovh0  30664  hmoval  31103  htth  31211  normval  31417  hlimi  31481  hsn0elch  31541  ocsh  31576  shscli  31610  shs00i  31743  chj00i  31780  riesz4i  32356  stm1addi  32538  stm1add3i  32540  superpos  32647  elrgspnlem2  33504  drnglring  33727  idlsrgmulrval  33744  splyval  33894  brfinext  33987  finextfldext  33999  irngval  34020  minplyval  34040  submateq  34144  metidv  34227  rmulccn  34263  pl1cn  34290  sibfof  34675  cxpcncf1  34927  subfacval2  35612  txsconnlem  35665  cvxpconn  35667  cvxsconn  35668  iscvm  35684  prv  35853  mpomulnzcnf  36734  knoppcnlem10  37014  bj-bary1  37878  ismblfin  38234  itg2addnclem3  38246  itg2addnc  38247  ftc1anclem3  38268  ftc1anc  38274  bfp  38397  rngo2  38480  rngohomco  38547  rngoisoval  38550  rngoisocnv  38554  crngohomfo  38579  keridl  38605  ispridlc  38643  snatpsubN  40448  cdlemn11pre  41908  dihord2pre  41923  baerlem3lem1  42405  prjcrvfval  43289  mendval  43832  mendplusg  43835  omcl3g  43987  mulvval  45102  fprodcnlem  46241  climf  46264  climf2  46306  cxpcncf2  46539  smflimlem3  47413  fmtnofac2lem  48243  prmdvdsfmtnof1lem2  48260  opoeALTV  48371  opeoALTV  48372  rngchomALTV  48956  funcringcsetcALTV2lem5  48982  ringchomALTV  48990  funcringcsetclem5ALTV  49005  srhmsubcALTVlem2  49012  srhmsubcALTV  49013  fldhmsubcALTV  49021  dmatALTval  49099  lincsumcl  49130  fdivval  49238  catprslem  49707  catprsc  49710  catprsc2  49711  oppcendc  49715  thincmoALT  50126  functhinclem2  50142  fullthinc2  50148  setc1onsubc  50299  lmdfval  50346  cmdfval  50347