Theorem oveq12 7396

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  (class class class)co 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  oveq12i  7399  oveq12d  7405  oveqan12d  7406  ovmpot  7550  mptmpoopabovd  8061  mptmpoopabovdOLD  8063  suppofssd  8182  sprmpod  8203  oev2  8487  oa00  8523  omopthi  8625  ecopoveq  8791  ecopovtrn  8793  isfsupp  9316  cantnffval  9616  ttrcltr  9669  fpwwe2lem4  10587  fpwwe2  10596  pwfseqlem4  10615  halfnq  10929  distrlem5pr  10980  addcmpblnr  11022  ltsrpr  11030  mulgt0sr  11058  add20  11690  msqge0  11699  recextlem2  11809  cru  12178  zaddcl  12573  qaddcl  12924  qmulcl  12926  xaddval  13183  xmulval  13185  xnn0xadd0  13207  xadddilem  13254  fzopth  13522  fzoopth  13723  modval  13833  1exp  14056  m1expeven  14074  nn0opthi  14235  faclbnd  14255  faclbnd3  14257  bcn0  14275  ccatopth  14681  ccatopth2  14682  repswccat  14751  reval  15072  absval  15204  clim  15460  rlim  15461  fsumparts  15772  cpnnen  16197  dvds2add  16260  dvds2sub  16261  opoe  16333  omoe  16334  opeo  16335  omeo  16336  gcddvds  16473  gcdcl  16476  gcdeq0  16487  gcdneg  16492  gcdaddmlem  16494  bezoutlem3  16511  bezout  16513  gcddiv  16521  nn0rppwr  16531  eucalgval2  16551  lcmabs  16575  rpmul  16629  divgcdcoprmex  16636  isprm5  16677  prmexpb  16689  rpexp  16692  nn0gcdsq  16722  pcqmul  16824  prmreclem3  16889  mul4sq  16925  vdwapval  16944  f1ocpbl  17488  homfval  17653  comfval  17661  issect  17715  isfull  17874  isfth  17878  natfval  17911  catchom  18065  catcco  18067  funcsetcestrclem5  18120  plusfval  18574  0subm  18744  cycsubm  19134  cyccom  19135  isgim  19194  subgga  19232  cayleylem1  19342  lsmsubm  19583  subgdisjb  19623  pj1fval  19624  odadd1  19778  qusabl  19795  imasabl  19806  dprdsubg  19956  rnghmval  20349  isrngim  20354  dfrhm2  20383  isrhm  20387  isrim0OLD  20390  isrim0  20392  rhmval  20409  funcrngcsetcALT  20550  srhmsubclem3  20588  srhmsubc  20589  fldhmsubc  20694  scafval  20787  rmodislmodlem  20835  rmodislmod  20836  lss1d  20869  islmhm  20934  islmim  20969  pzriprnglem5  21395  pzriprnglem8  21398  znfld  21470  cygznlem3  21479  cnmsgnsubg  21486  psgnghm  21489  ipeq0  21547  ipfval  21558  dsmmval  21643  dsmmacl  21650  mplval  21898  mplcoe5lem  21946  opsrval  21953  evlval  22002  mpfind  22014  selvffval  22020  mhpfval  22025  mhpmulcl  22036  psdffval  22044  mat1dimcrng  22364  dmatval  22379  dmatmulcl  22387  scmatval  22391  scmataddcl  22403  scmatsubcl  22404  scmatmulcl  22405  mavmul0g  22440  marrepfval  22447  marrepeval  22450  marepvfval  22452  marepveval  22455  submafval  22466  submaeval  22469  mdetfval  22473  madugsum  22530  minmar1fval  22533  minmar1eval  22536  symgmatr01  22541  gsummatr01lem3  22544  gsummatr01lem4  22545  gsummatr01  22546  cpmatacl  22603  mat2pmatfval  22610  mat2pmatvalel  22612  mat2pmatmul  22618  cpm2mfval  22636  cpm2mvalel  22638  m2cpminvid  22640  m2cpminvid2  22642  decpmate  22653  pmatcollpw1  22663  monmatcollpw  22666  pmatcollpwlem  22667  pmatcollpw  22668  pmatcollpwscmatlem2  22677  pm2mpval  22682  pm2mpf1  22686  mp2pm2mplem3  22695  mp2pm2mplem4  22696  chpmatfval  22717  tx2ndc  23538  cnmpt2t  23560  cnmpt22f  23562  hmeofval  23645  qustgplem  24008  stdbdmetval  24402  nmofval  24602  nghmfval  24610  isnmhm  24634  xrsxmet  24698  divcn  24759  divccn  24764  iihalf1cn  24826  iihalf2cn  24829  icchmeo  24838  cnrehmeo  24851  isphtpy  24880  isphtpc  24893  reparphti  24896  pcorevlem  24926  cphnm  25093  tcphnmval  25129  ipcau2  25134  tcphcphlem1  25135  tcphcphlem2  25136  tcphcph  25137  bcthlem1  25224  bcth  25229  mulcncf  25346  dyadmax  25499  volcn  25507  vitalilem1  25509  vitalilem2  25510  vitalilem3  25511  vitali  25514  i1fmullem  25595  itg1addlem4  25600  dvlip  25898  ftc1a  25944  mdegfval  25967  r1pval  26063  coeaddlem  26154  plycn  26166  quotval  26200  elqaalem2  26228  taylfval  26266  psercn2  26332  cxpcn  26654  cxpcn3  26658  resqrtcn  26659  sqrtcn  26660  abscxpbnd  26663  angval  26711  chordthmlem  26742  dcubic  26756  efrlim  26879  lgsdchr  27266  mul2sq  27330  ostthlem2  27539  zaddscl  28282  zmulscld  28285  zseo  28308  tglngval  28478  islnopp  28666  ishpg  28686  finsumvtxdg2size  29478  wspthsn  29778  wwlksnon  29781  wspthsnon  29782  iswspthsnon  29786  2clwwlk  30276  numclwlk1lem2  30299  numclwwlkovh0  30301  hmoval  30739  htth  30847  normval  31053  hlimi  31117  hsn0elch  31177  ocsh  31212  shscli  31246  shs00i  31379  chj00i  31416  riesz4i  31992  stm1addi  32174  stm1add3i  32176  superpos  32283  elrgspnlem2  33194  prmidlc  33419  idlsrgmulrval  33480  brfinext  33648  irngval  33680  minplyval  33695  submateq  33799  metidv  33882  rmulccn  33918  pl1cn  33945  sibfof  34331  cxpcncf1  34586  subfacval2  35174  txsconnlem  35227  cvxpconn  35229  cvxsconn  35230  iscvm  35246  prv  35415  mpomulnzcnf  36287  knoppcnlem10  36490  bj-bary1  37300  ismblfin  37655  itg2addnclem3  37667  itg2addnc  37668  ftc1anclem3  37689  ftc1anc  37695  bfp  37818  rngo2  37901  rngohomco  37968  rngoisoval  37971  rngoisocnv  37975  crngohomfo  38000  keridl  38026  ispridlc  38064  snatpsubN  39744  cdlemn11pre  41204  dihord2pre  41219  baerlem3lem1  41701  prjcrvfval  42619  mendval  43168  mendplusg  43171  omcl3g  43323  mulvval  44457  fprodcnlem  45597  climf  45620  climf2  45664  cxpcncf2  45897  smflimlem3  46771  fmtnofac2lem  47569  prmdvdsfmtnof1lem2  47586  opoeALTV  47684  opeoALTV  47685  rngchomALTV  48256  funcringcsetcALTV2lem5  48282  ringchomALTV  48290  funcringcsetclem5ALTV  48305  srhmsubcALTVlem2  48312  srhmsubcALTV  48313  fldhmsubcALTV  48321  dmatALTval  48389  lincsumcl  48420  fdivval  48528  catprslem  48999  catprsc  49002  catprsc2  49003  oppcendc  49007  thincmoALT  49418  functhinclem2  49434  fullthinc2  49440  setc1onsubc  49591  lmdfval  49638  cmdfval  49639