Theorem oveq12 7440

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434

This theorem is referenced by:  oveq12i  7443  oveq12d  7449  oveqan12d  7450  ovmpot  7594  mptmpoopabovd  8106  mptmpoopabovdOLD  8108  suppofssd  8227  sprmpod  8248  oev2  8560  oa00  8596  omopthi  8698  ecopoveq  8857  ecopovtrn  8859  isfsupp  9403  cantnffval  9701  ttrcltr  9754  fpwwe2lem4  10672  fpwwe2  10681  pwfseqlem4  10700  halfnq  11014  distrlem5pr  11065  addcmpblnr  11107  ltsrpr  11115  mulgt0sr  11143  add20  11773  msqge0  11782  recextlem2  11892  cru  12256  zaddcl  12655  qaddcl  13005  qmulcl  13007  xaddval  13262  xmulval  13264  xnn0xadd0  13286  xadddilem  13333  fzopth  13598  fzoopth  13798  modval  13908  1exp  14129  m1expeven  14147  nn0opthi  14306  faclbnd  14326  faclbnd3  14328  bcn0  14346  ccatopth  14751  ccatopth2  14752  repswccat  14821  reval  15142  absval  15274  clim  15527  rlim  15528  fsumparts  15839  cpnnen  16262  dvds2add  16324  dvds2sub  16325  opoe  16397  omoe  16398  opeo  16399  omeo  16400  gcddvds  16537  gcdcl  16540  gcdeq0  16551  gcdneg  16556  gcdaddmlem  16558  bezoutlem3  16575  bezout  16577  gcddiv  16585  nn0rppwr  16595  eucalgval2  16615  lcmabs  16639  rpmul  16693  divgcdcoprmex  16700  isprm5  16741  prmexpb  16753  rpexp  16756  nn0gcdsq  16786  pcqmul  16887  prmreclem3  16952  mul4sq  16988  vdwapval  17007  f1ocpbl  17572  homfval  17737  comfval  17745  issect  17801  isfull  17964  isfth  17968  natfval  18001  catchom  18157  catcco  18159  funcsetcestrclem5  18215  plusfval  18673  0subm  18843  cycsubm  19233  cyccom  19234  isgim  19293  subgga  19331  cayleylem1  19445  lsmsubm  19686  subgdisjb  19726  pj1fval  19727  odadd1  19881  qusabl  19898  imasabl  19909  dprdsubg  20059  rnghmval  20457  isrngim  20462  dfrhm2  20491  isrhm  20495  isrim0OLD  20498  isrim0  20500  rhmval  20517  funcrngcsetcALT  20658  srhmsubclem3  20696  srhmsubc  20697  fldhmsubc  20803  scafval  20896  rmodislmodlem  20944  rmodislmod  20945  rmodislmodOLD  20946  lss1d  20979  islmhm  21044  islmim  21079  pzriprnglem5  21514  pzriprnglem8  21517  znfld  21597  cygznlem3  21606  cnmsgnsubg  21613  psgnghm  21616  ipeq0  21674  ipfval  21685  dsmmval  21772  dsmmacl  21779  mplval  22027  mplcoe5lem  22075  opsrval  22082  evlval  22137  mpfind  22149  selvffval  22155  mhpfval  22160  mhpmulcl  22171  psdffval  22179  mat1dimcrng  22499  dmatval  22514  dmatmulcl  22522  scmatval  22526  scmataddcl  22538  scmatsubcl  22539  scmatmulcl  22540  mavmul0g  22575  marrepfval  22582  marrepeval  22585  marepvfval  22587  marepveval  22590  submafval  22601  submaeval  22604  mdetfval  22608  madugsum  22665  minmar1fval  22668  minmar1eval  22671  symgmatr01  22676  gsummatr01lem3  22679  gsummatr01lem4  22680  gsummatr01  22681  cpmatacl  22738  mat2pmatfval  22745  mat2pmatvalel  22747  mat2pmatmul  22753  cpm2mfval  22771  cpm2mvalel  22773  m2cpminvid  22775  m2cpminvid2  22777  decpmate  22788  pmatcollpw1  22798  monmatcollpw  22801  pmatcollpwlem  22802  pmatcollpw  22803  pmatcollpwscmatlem2  22812  pm2mpval  22817  pm2mpf1  22821  mp2pm2mplem3  22830  mp2pm2mplem4  22831  chpmatfval  22852  tx2ndc  23675  cnmpt2t  23697  cnmpt22f  23699  hmeofval  23782  qustgplem  24145  stdbdmetval  24543  nmofval  24751  nghmfval  24759  isnmhm  24783  xrsxmet  24845  divcn  24906  divccn  24911  iihalf1cn  24973  iihalf2cn  24976  icchmeo  24985  cnrehmeo  24998  isphtpy  25027  isphtpc  25040  reparphti  25043  pcorevlem  25073  cphnm  25241  tcphnmval  25277  ipcau2  25282  tcphcphlem1  25283  tcphcphlem2  25284  tcphcph  25285  bcthlem1  25372  bcth  25377  mulcncf  25494  dyadmax  25647  volcn  25655  vitalilem1  25657  vitalilem2  25658  vitalilem3  25659  vitali  25662  i1fmullem  25743  itg1addlem4  25748  itg1addlem4OLD  25749  dvlip  26047  ftc1a  26093  mdegfval  26116  r1pval  26212  coeaddlem  26303  plycn  26315  quotval  26349  elqaalem2  26377  taylfval  26415  psercn2  26481  cxpcn  26802  cxpcn3  26806  resqrtcn  26807  sqrtcn  26808  abscxpbnd  26811  angval  26859  chordthmlem  26890  dcubic  26904  efrlim  27027  lgsdchr  27414  mul2sq  27478  ostthlem2  27687  zaddscl  28395  zmulscld  28398  zseo  28421  tglngval  28574  islnopp  28762  ishpg  28782  finsumvtxdg2size  29583  wspthsn  29878  wwlksnon  29881  wspthsnon  29882  iswspthsnon  29886  2clwwlk  30376  numclwlk1lem2  30399  numclwwlkovh0  30401  hmoval  30839  htth  30947  normval  31153  hlimi  31217  hsn0elch  31277  ocsh  31312  shscli  31346  shs00i  31479  chj00i  31516  riesz4i  32092  stm1addi  32274  stm1add3i  32276  superpos  32383  elrgspnlem2  33233  prmidlc  33456  idlsrgmulrval  33517  brfinext  33681  irngval  33700  minplyval  33713  fldext2chn  33734  submateq  33770  metidv  33853  rmulccn  33889  pl1cn  33916  sibfof  34322  cxpcncf1  34589  subfacval2  35172  txsconnlem  35225  cvxpconn  35227  cvxsconn  35228  iscvm  35244  prv  35413  mpomulnzcnf  36282  knoppcnlem10  36485  bj-bary1  37295  ismblfin  37648  itg2addnclem3  37660  itg2addnc  37661  ftc1anclem3  37682  ftc1anc  37688  bfp  37811  rngo2  37894  rngohomco  37961  rngoisoval  37964  rngoisocnv  37968  crngohomfo  37993  keridl  38019  ispridlc  38057  snatpsubN  39733  cdlemn11pre  41193  dihord2pre  41208  baerlem3lem1  41690  sn-inelr  42474  prjcrvfval  42618  mendval  43168  mendplusg  43171  omcl3g  43324  mulvval  44464  fprodcnlem  45555  climf  45578  climf2  45622  cxpcncf2  45855  smflimlem3  46729  fmtnofac2lem  47493  prmdvdsfmtnof1lem2  47510  opoeALTV  47608  opeoALTV  47609  rngchomALTV  48112  funcringcsetcALTV2lem5  48138  ringchomALTV  48146  funcringcsetclem5ALTV  48161  srhmsubcALTVlem2  48168  srhmsubcALTV  48169  fldhmsubcALTV  48177  dmatALTval  48246  lincsumcl  48277  fdivval  48389  catprslem  48799  catprsc  48802  catprsc2  48803  thincmoALT  48830  functhinclem2  48842  fullthinc2  48847