Theorem oveq12 6558

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  (class class class)co 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  oveq12i  6561  oveq12d  6567  oveqan12d  6568  sprmpt2d  7237  oev2  7490  oa00  7526  omopthi  7624  ecopoveq  7735  ecopovtrn  7737  isfsupp  8162  cantnffval  8443  fpwwe2  9344  halfnq  9677  distrlem5pr  9728  addcmpblnr  9769  ltsrpr  9777  mulgt0sr  9805  add20  10419  msqge0  10428  recextlem2  10537  cru  10889  zaddcl  11294  qaddcl  11680  qmulcl  11682  xaddval  11928  xmulval  11930  xnn0xadd0  11949  xadddilem  11996  fzopth  12249  modval  12532  1exp  12751  m1expeven  12769  nn0opthi  12919  faclbnd  12939  faclbnd3  12941  bcn0  12959  ccatopth  13322  ccatopth2  13323  repswccat  13383  reval  13694  absval  13826  clim  14073  rlim  14074  fsumparts  14379  cpnnen  14797  dvds2add  14853  dvds2sub  14854  opoe  14925  omoe  14926  opeo  14927  omeo  14928  gcddvds  15063  gcdcl  15066  gcdeq0  15076  gcdneg  15081  gcdaddmlem  15083  gcdabs  15088  bezoutlem3  15096  bezout  15098  gcddiv  15106  eucalgval2  15132  lcmabs  15156  rpmul  15211  divgcdcoprmex  15218  isprm5  15257  prmexpb  15268  rpexp  15270  nn0gcdsq  15298  pcqmul  15396  prmreclem3  15460  mul4sq  15496  vdwapval  15515  f1ocpbl  16008  homfval  16175  comfval  16183  issect  16236  isfull  16393  isfth  16397  natfval  16429  catchom  16572  catcco  16574  funcsetcestrclem5  16622  plusfval  17071  isgim  17527  subgga  17556  cayleylem1  17655  lsmsubm  17891  subgdisjb  17929  pj1fval  17930  odadd1  18074  qusabl  18091  cygabl  18115  dprdsubg  18246  ringadd2  18398  dfrhm2  18540  isrhm  18544  isrim0  18546  scafval  18705  lss1d  18784  islmhm  18848  islmim  18883  mplval  19249  mplcoe5lem  19288  opsrval  19295  evlval  19345  mpfind  19357  znfld  19728  cygznlem3  19737  cnmsgnsubg  19742  psgnghm  19745  ipeq0  19802  ipfval  19813  dsmmval  19897  dsmmacl  19904  mat1dimcrng  20102  dmatval  20117  dmatmulcl  20125  scmatval  20129  scmataddcl  20141  scmatsubcl  20142  scmatmulcl  20143  mavmul0g  20178  marrepfval  20185  marrepeval  20188  marepvfval  20190  marepveval  20193  submafval  20204  submaeval  20207  mdetfval  20211  madugsum  20268  minmar1fval  20271  minmar1eval  20274  symgmatr01  20279  gsummatr01lem3  20282  gsummatr01lem4  20283  gsummatr01  20284  cpmatacl  20340  mat2pmatfval  20347  mat2pmatvalel  20349  mat2pmatmul  20355  cpm2mfval  20373  cpm2mvalel  20375  m2cpminvid  20377  m2cpminvid2  20379  decpmate  20390  pmatcollpw1  20400  monmatcollpw  20403  pmatcollpwlem  20404  pmatcollpw  20405  pmatcollpwscmatlem2  20414  pm2mpval  20419  pm2mpf1  20423  mp2pm2mplem3  20432  mp2pm2mplem4  20433  chpmatfval  20454  tx2ndc  21264  cnmpt2t  21286  cnmpt22f  21288  hmeofval  21371  qustgplem  21734  stdbdmetval  22129  nmofval  22328  nghmfval  22336  isnmhm  22360  xrsxmet  22420  isphtpy  22588  isphtpc  22601  pcorevlem  22634  cphnm  22801  tchnmval  22836  ipcau2  22841  tchcphlem1  22842  tchcphlem2  22843  tchcph  22844  bcthlem1  22929  bcth  22934  dyadmax  23172  volcn  23180  vitalilem1  23182  vitalilem1OLD  23183  vitalilem2  23184  vitalilem3  23185  vitali  23188  i1fmullem  23267  itg1addlem4  23272  dvlip  23560  ftc1a  23604  mdegfval  23626  r1pval  23720  coeaddlem  23809  quotval  23851  elqaalem2  23879  taylfval  23917  cxpcn3  24289  resqrtcn  24290  sqrtcn  24291  abscxpbnd  24294  angval  24331  chordthmlem  24359  dcubic  24373  lgsdchr  24880  mul2sq  24944  ostthlem2  25117  tglngval  25246  islnopp  25431  ishpg  25451  wlkon  26061  wlkonprop  26063  trls  26066  trlon  26070  trlonprop  26072  pths  26096  spths  26097  pthon  26105  pthonprop  26107  spthon  26112  spthonprp  26115  isconngra  26200  isconngra1  26201  wwlkn  26210  clwlk  26281  clwlkcompim  26292  clwwlkn  26295  clwwlknprop  26300  is2wlkonot  26390  is2spthonot  26391  2wlkonot  26392  2spthonot  26393  2wlksot  26394  2spthsot  26395  2wlkonot3v  26402  2spthonot3v  26403  isrgra  26453  hmoval  27049  htth  27159  normval  27365  hlimi  27429  hsn0elch  27489  ocsh  27526  shscli  27560  shs00i  27693  chj00i  27730  riesz4i  28306  stm1addi  28488  stm1add3i  28490  superpos  28597  submateq  29203  metidv  29263  rmulccn  29302  pl1cn  29329  sibfof  29729  subfacval2  30423  txsconlem  30476  iscvm  30495  bj-bary1  32339  ismblfin  32620  itg2addnclem3  32633  itg2addnc  32634  ftc1anclem3  32657  ftc1anc  32663  bfp  32793  rngo2  32876  rngohomco  32943  rngoisoval  32946  rngoisocnv  32950  crngohomfo  32975  keridl  33001  ispridlc  33039  snatpsubN  34054  cdlemn11pre  35517  dihord2pre  35532  baerlem3lem1  36014  mendval  36772  mendplusg  36775  mulvval  37693  climf  38689  climf2  38733  cxpcncf2  38786  smflimlem3  39659  fmtnofac2lem  40018  prmdvdsfmtnof1lem2  40035  opoeALTV  40132  opeoALTV  40133  mptmpt2opabovd  40336  fzoopth  40360  wspthsn  41046  wwlksnon  41049  wspthsnon  41050  iswspthsnon  41052  rnghmval  41681  isrngisom  41686  rhmval  41709  rngchomALTV  41777  funcrngcsetcALT  41791  funcringcsetcALTV2lem5  41832  ringchomALTV  41840  funcringcsetclem5ALTV  41855  srhmsubclem3  41867  srhmsubc  41868  fldhmsubc  41876  srhmsubcALTVlem3  41886  srhmsubcALTV  41887  fldhmsubcALTV  41895  dmatALTval  41983  lincsumcl  42014  fdivval  42131