Theorem oveq12 7378

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

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  oveq12i  7381  oveq12d  7387  oveqan12d  7388  ovmpot  7530  mptmpoopabovd  8040  suppofssd  8159  sprmpod  8180  oev2  8464  oa00  8500  omopthi  8602  ecopoveq  8768  ecopovtrn  8770  isfsupp  9292  cantnffval  9592  ttrcltr  9645  fpwwe2lem4  10563  fpwwe2  10572  pwfseqlem4  10591  halfnq  10905  distrlem5pr  10956  addcmpblnr  10998  ltsrpr  11006  mulgt0sr  11034  add20  11666  msqge0  11675  recextlem2  11785  cru  12154  zaddcl  12549  qaddcl  12900  qmulcl  12902  xaddval  13159  xmulval  13161  xnn0xadd0  13183  xadddilem  13230  fzopth  13498  fzoopth  13699  modval  13809  1exp  14032  m1expeven  14050  nn0opthi  14211  faclbnd  14231  faclbnd3  14233  bcn0  14251  ccatopth  14657  ccatopth2  14658  repswccat  14727  reval  15048  absval  15180  clim  15436  rlim  15437  fsumparts  15748  cpnnen  16173  dvds2add  16236  dvds2sub  16237  opoe  16309  omoe  16310  opeo  16311  omeo  16312  gcddvds  16449  gcdcl  16452  gcdeq0  16463  gcdneg  16468  gcdaddmlem  16470  bezoutlem3  16487  bezout  16489  gcddiv  16497  nn0rppwr  16507  eucalgval2  16527  lcmabs  16551  rpmul  16605  divgcdcoprmex  16612  isprm5  16653  prmexpb  16665  rpexp  16668  nn0gcdsq  16698  pcqmul  16800  prmreclem3  16865  mul4sq  16901  vdwapval  16920  f1ocpbl  17464  homfval  17633  comfval  17641  issect  17695  isfull  17854  isfth  17858  natfval  17891  catchom  18045  catcco  18047  funcsetcestrclem5  18100  plusfval  18556  0subm  18726  cycsubm  19116  cyccom  19117  isgim  19176  subgga  19214  cayleylem1  19326  lsmsubm  19567  subgdisjb  19607  pj1fval  19608  odadd1  19762  qusabl  19779  imasabl  19790  dprdsubg  19940  rnghmval  20360  isrngim  20365  dfrhm2  20394  isrhm  20398  isrim0OLD  20401  isrim0  20403  rhmval  20420  funcrngcsetcALT  20561  srhmsubclem3  20599  srhmsubc  20600  fldhmsubc  20705  scafval  20819  rmodislmodlem  20867  rmodislmod  20868  lss1d  20901  islmhm  20966  islmim  21001  pzriprnglem5  21427  pzriprnglem8  21430  znfld  21502  cygznlem3  21511  cnmsgnsubg  21519  psgnghm  21522  ipeq0  21580  ipfval  21591  dsmmval  21676  dsmmacl  21683  mplval  21931  mplcoe5lem  21979  opsrval  21986  evlval  22035  mpfind  22047  selvffval  22053  mhpfval  22058  mhpmulcl  22069  psdffval  22077  mat1dimcrng  22397  dmatval  22412  dmatmulcl  22420  scmatval  22424  scmataddcl  22436  scmatsubcl  22437  scmatmulcl  22438  mavmul0g  22473  marrepfval  22480  marrepeval  22483  marepvfval  22485  marepveval  22488  submafval  22499  submaeval  22502  mdetfval  22506  madugsum  22563  minmar1fval  22566  minmar1eval  22569  symgmatr01  22574  gsummatr01lem3  22577  gsummatr01lem4  22578  gsummatr01  22579  cpmatacl  22636  mat2pmatfval  22643  mat2pmatvalel  22645  mat2pmatmul  22651  cpm2mfval  22669  cpm2mvalel  22671  m2cpminvid  22673  m2cpminvid2  22675  decpmate  22686  pmatcollpw1  22696  monmatcollpw  22699  pmatcollpwlem  22700  pmatcollpw  22701  pmatcollpwscmatlem2  22710  pm2mpval  22715  pm2mpf1  22719  mp2pm2mplem3  22728  mp2pm2mplem4  22729  chpmatfval  22750  tx2ndc  23571  cnmpt2t  23593  cnmpt22f  23595  hmeofval  23678  qustgplem  24041  stdbdmetval  24435  nmofval  24635  nghmfval  24643  isnmhm  24667  xrsxmet  24731  divcn  24792  divccn  24797  iihalf1cn  24859  iihalf2cn  24862  icchmeo  24871  cnrehmeo  24884  isphtpy  24913  isphtpc  24926  reparphti  24929  pcorevlem  24959  cphnm  25126  tcphnmval  25162  ipcau2  25167  tcphcphlem1  25168  tcphcphlem2  25169  tcphcph  25170  bcthlem1  25257  bcth  25262  mulcncf  25379  dyadmax  25532  volcn  25540  vitalilem1  25542  vitalilem2  25543  vitalilem3  25544  vitali  25547  i1fmullem  25628  itg1addlem4  25633  dvlip  25931  ftc1a  25977  mdegfval  26000  r1pval  26096  coeaddlem  26187  plycn  26199  quotval  26233  elqaalem2  26261  taylfval  26299  psercn2  26365  cxpcn  26687  cxpcn3  26691  resqrtcn  26692  sqrtcn  26693  abscxpbnd  26696  angval  26744  chordthmlem  26775  dcubic  26789  efrlim  26912  lgsdchr  27299  mul2sq  27363  ostthlem2  27572  zaddscl  28322  zmulscld  28325  zseo  28349  zs12addscl  28389  tglngval  28531  islnopp  28719  ishpg  28739  finsumvtxdg2size  29531  wspthsn  29828  wwlksnon  29831  wspthsnon  29832  iswspthsnon  29836  2clwwlk  30326  numclwlk1lem2  30349  numclwwlkovh0  30351  hmoval  30789  htth  30897  normval  31103  hlimi  31167  hsn0elch  31227  ocsh  31262  shscli  31296  shs00i  31429  chj00i  31466  riesz4i  32042  stm1addi  32224  stm1add3i  32226  superpos  32333  elrgspnlem2  33210  prmidlc  33412  idlsrgmulrval  33473  brfinext  33641  irngval  33673  minplyval  33688  submateq  33792  metidv  33875  rmulccn  33911  pl1cn  33938  sibfof  34324  cxpcncf1  34579  subfacval2  35167  txsconnlem  35220  cvxpconn  35222  cvxsconn  35223  iscvm  35239  prv  35408  mpomulnzcnf  36280  knoppcnlem10  36483  bj-bary1  37293  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  39737  cdlemn11pre  41197  dihord2pre  41212  baerlem3lem1  41694  prjcrvfval  42612  mendval  43161  mendplusg  43164  omcl3g  43316  mulvval  44450  fprodcnlem  45590  climf  45613  climf2  45657  cxpcncf2  45890  smflimlem3  46764  fmtnofac2lem  47562  prmdvdsfmtnof1lem2  47579  opoeALTV  47677  opeoALTV  47678  rngchomALTV  48249  funcringcsetcALTV2lem5  48275  ringchomALTV  48283  funcringcsetclem5ALTV  48298  srhmsubcALTVlem2  48305  srhmsubcALTV  48306  fldhmsubcALTV  48314  dmatALTval  48382  lincsumcl  48413  fdivval  48521  catprslem  48992  catprsc  48995  catprsc2  48996  oppcendc  49000  thincmoALT  49411  functhinclem2  49427  fullthinc2  49433  setc1onsubc  49584  lmdfval  49631  cmdfval  49632