Theorem oveq12 6659

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483  (class class class)co 6650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  oveq12i  6662  oveq12d  6668  oveqan12d  6669  mptmpt2opabovd  7249  sprmpt2d  7350  oev2  7603  oa00  7639  omopthi  7737  ecopoveq  7848  ecopovtrn  7850  isfsupp  8279  cantnffval  8560  fpwwe2  9465  halfnq  9798  distrlem5pr  9849  addcmpblnr  9890  ltsrpr  9898  mulgt0sr  9926  add20  10540  msqge0  10549  recextlem2  10658  cru  11012  zaddcl  11417  qaddcl  11804  qmulcl  11806  xaddval  12054  xmulval  12056  xnn0xadd0  12077  xadddilem  12124  fzopth  12378  modval  12670  1exp  12889  m1expeven  12907  nn0opthi  13057  faclbnd  13077  faclbnd3  13079  bcn0  13097  ccatopth  13470  ccatopth2  13471  repswccat  13532  reval  13846  absval  13978  clim  14225  rlim  14226  fsumparts  14538  cpnnen  14958  dvds2add  15015  dvds2sub  15016  opoe  15087  omoe  15088  opeo  15089  omeo  15090  gcddvds  15225  gcdcl  15228  gcdeq0  15238  gcdneg  15243  gcdaddmlem  15245  gcdabs  15250  bezoutlem3  15258  bezout  15260  gcddiv  15268  eucalgval2  15294  lcmabs  15318  rpmul  15373  divgcdcoprmex  15380  isprm5  15419  prmexpb  15430  rpexp  15432  nn0gcdsq  15460  pcqmul  15558  prmreclem3  15622  mul4sq  15658  vdwapval  15677  f1ocpbl  16185  homfval  16352  comfval  16360  issect  16413  isfull  16570  isfth  16574  natfval  16606  catchom  16749  catcco  16751  funcsetcestrclem5  16799  plusfval  17248  isgim  17704  subgga  17733  cayleylem1  17832  lsmsubm  18068  subgdisjb  18106  pj1fval  18107  odadd1  18251  qusabl  18268  cygabl  18292  dprdsubg  18423  ringadd2  18575  dfrhm2  18717  isrhm  18721  isrim0  18723  scafval  18882  rmodislmodlem  18930  rmodislmod  18931  lss1d  18963  islmhm  19027  islmim  19062  mplval  19428  mplcoe5lem  19467  opsrval  19474  evlval  19524  mpfind  19536  znfld  19909  cygznlem3  19918  cnmsgnsubg  19923  psgnghm  19926  ipeq0  19983  ipfval  19994  dsmmval  20078  dsmmacl  20085  mat1dimcrng  20283  dmatval  20298  dmatmulcl  20306  scmatval  20310  scmataddcl  20322  scmatsubcl  20323  scmatmulcl  20324  mavmul0g  20359  marrepfval  20366  marrepeval  20369  marepvfval  20371  marepveval  20374  submafval  20385  submaeval  20388  mdetfval  20392  madugsum  20449  minmar1fval  20452  minmar1eval  20455  symgmatr01  20460  gsummatr01lem3  20463  gsummatr01lem4  20464  gsummatr01  20465  cpmatacl  20521  mat2pmatfval  20528  mat2pmatvalel  20530  mat2pmatmul  20536  cpm2mfval  20554  cpm2mvalel  20556  m2cpminvid  20558  m2cpminvid2  20560  decpmate  20571  pmatcollpw1  20581  monmatcollpw  20584  pmatcollpwlem  20585  pmatcollpw  20586  pmatcollpwscmatlem2  20595  pm2mpval  20600  pm2mpf1  20604  mp2pm2mplem3  20613  mp2pm2mplem4  20614  chpmatfval  20635  tx2ndc  21454  cnmpt2t  21476  cnmpt22f  21478  hmeofval  21561  qustgplem  21924  stdbdmetval  22319  nmofval  22518  nghmfval  22526  isnmhm  22550  xrsxmet  22612  isphtpy  22780  isphtpc  22793  pcorevlem  22826  cphnm  22993  tchnmval  23028  ipcau2  23033  tchcphlem1  23034  tchcphlem2  23035  tchcph  23036  bcthlem1  23121  bcth  23126  dyadmax  23366  volcn  23374  vitalilem1  23376  vitalilem1OLD  23377  vitalilem2  23378  vitalilem3  23379  vitali  23382  i1fmullem  23461  itg1addlem4  23466  dvlip  23756  ftc1a  23800  mdegfval  23822  r1pval  23916  coeaddlem  24005  quotval  24047  elqaalem2  24075  taylfval  24113  cxpcn3  24489  resqrtcn  24490  sqrtcn  24491  abscxpbnd  24494  angval  24531  chordthmlem  24559  dcubic  24573  lgsdchr  25080  mul2sq  25144  ostthlem2  25317  tglngval  25446  islnopp  25631  ishpg  25651  finsumvtxdg2size  26446  wspthsn  26735  wwlksnon  26738  wspthsnon  26739  iswspthsnon  26741  hmoval  27665  htth  27775  normval  27981  hlimi  28045  hsn0elch  28105  ocsh  28142  shscli  28176  shs00i  28309  chj00i  28346  riesz4i  28922  stm1addi  29104  stm1add3i  29106  superpos  29213  submateq  29875  metidv  29935  rmulccn  29974  pl1cn  30001  sibfof  30402  cxpcncf1  30673  subfacval2  31169  txsconnlem  31222  iscvm  31241  bj-bary1  33162  ismblfin  33450  itg2addnclem3  33463  itg2addnc  33464  ftc1anclem3  33487  ftc1anc  33493  bfp  33623  rngo2  33706  rngohomco  33773  rngoisoval  33776  rngoisocnv  33780  crngohomfo  33805  keridl  33831  ispridlc  33869  snatpsubN  35036  cdlemn11pre  36499  dihord2pre  36514  baerlem3lem1  36996  mendval  37753  mendplusg  37756  mulvval  38672  climf  39854  climf2  39898  cxpcncf2  40113  smflimlem3  40981  fzoopth  41337  fmtnofac2lem  41480  prmdvdsfmtnof1lem2  41497  opoeALTV  41594  opeoALTV  41595  rnghmval  41891  isrngisom  41896  rhmval  41919  rngchomALTV  41985  funcrngcsetcALT  41999  funcringcsetcALTV2lem5  42040  ringchomALTV  42048  funcringcsetclem5ALTV  42063  srhmsubclem3  42075  srhmsubc  42076  fldhmsubc  42084  srhmsubcALTVlem2  42093  srhmsubcALTV  42094  fldhmsubcALTV  42102  dmatALTval  42189  lincsumcl  42220  fdivval  42333