Theorem oveq12 7419

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413

This theorem is referenced by:  oveq12i  7422  oveq12d  7428  oveqan12d  7429  ovmpot  7573  mptmpoopabovd  8086  mptmpoopabovdOLD  8088  suppofssd  8207  sprmpod  8228  oev2  8540  oa00  8576  omopthi  8678  ecopoveq  8837  ecopovtrn  8839  isfsupp  9382  cantnffval  9682  ttrcltr  9735  fpwwe2lem4  10653  fpwwe2  10662  pwfseqlem4  10681  halfnq  10995  distrlem5pr  11046  addcmpblnr  11088  ltsrpr  11096  mulgt0sr  11124  add20  11754  msqge0  11763  recextlem2  11873  cru  12237  zaddcl  12637  qaddcl  12986  qmulcl  12988  xaddval  13244  xmulval  13246  xnn0xadd0  13268  xadddilem  13315  fzopth  13583  fzoopth  13783  modval  13893  1exp  14114  m1expeven  14132  nn0opthi  14293  faclbnd  14313  faclbnd3  14315  bcn0  14333  ccatopth  14739  ccatopth2  14740  repswccat  14809  reval  15130  absval  15262  clim  15515  rlim  15516  fsumparts  15827  cpnnen  16252  dvds2add  16314  dvds2sub  16315  opoe  16387  omoe  16388  opeo  16389  omeo  16390  gcddvds  16527  gcdcl  16530  gcdeq0  16541  gcdneg  16546  gcdaddmlem  16548  bezoutlem3  16565  bezout  16567  gcddiv  16575  nn0rppwr  16585  eucalgval2  16605  lcmabs  16629  rpmul  16683  divgcdcoprmex  16690  isprm5  16731  prmexpb  16743  rpexp  16746  nn0gcdsq  16776  pcqmul  16878  prmreclem3  16943  mul4sq  16979  vdwapval  16998  f1ocpbl  17544  homfval  17709  comfval  17717  issect  17771  isfull  17930  isfth  17934  natfval  17967  catchom  18121  catcco  18123  funcsetcestrclem5  18176  plusfval  18630  0subm  18800  cycsubm  19190  cyccom  19191  isgim  19250  subgga  19288  cayleylem1  19398  lsmsubm  19639  subgdisjb  19679  pj1fval  19680  odadd1  19834  qusabl  19851  imasabl  19862  dprdsubg  20012  rnghmval  20405  isrngim  20410  dfrhm2  20439  isrhm  20443  isrim0OLD  20446  isrim0  20448  rhmval  20465  funcrngcsetcALT  20606  srhmsubclem3  20644  srhmsubc  20645  fldhmsubc  20750  scafval  20843  rmodislmodlem  20891  rmodislmod  20892  lss1d  20925  islmhm  20990  islmim  21025  pzriprnglem5  21451  pzriprnglem8  21454  znfld  21526  cygznlem3  21535  cnmsgnsubg  21542  psgnghm  21545  ipeq0  21603  ipfval  21614  dsmmval  21699  dsmmacl  21706  mplval  21954  mplcoe5lem  22002  opsrval  22009  evlval  22058  mpfind  22070  selvffval  22076  mhpfval  22081  mhpmulcl  22092  psdffval  22100  mat1dimcrng  22420  dmatval  22435  dmatmulcl  22443  scmatval  22447  scmataddcl  22459  scmatsubcl  22460  scmatmulcl  22461  mavmul0g  22496  marrepfval  22503  marrepeval  22506  marepvfval  22508  marepveval  22511  submafval  22522  submaeval  22525  mdetfval  22529  madugsum  22586  minmar1fval  22589  minmar1eval  22592  symgmatr01  22597  gsummatr01lem3  22600  gsummatr01lem4  22601  gsummatr01  22602  cpmatacl  22659  mat2pmatfval  22666  mat2pmatvalel  22668  mat2pmatmul  22674  cpm2mfval  22692  cpm2mvalel  22694  m2cpminvid  22696  m2cpminvid2  22698  decpmate  22709  pmatcollpw1  22719  monmatcollpw  22722  pmatcollpwlem  22723  pmatcollpw  22724  pmatcollpwscmatlem2  22733  pm2mpval  22738  pm2mpf1  22742  mp2pm2mplem3  22751  mp2pm2mplem4  22752  chpmatfval  22773  tx2ndc  23594  cnmpt2t  23616  cnmpt22f  23618  hmeofval  23701  qustgplem  24064  stdbdmetval  24458  nmofval  24658  nghmfval  24666  isnmhm  24690  xrsxmet  24754  divcn  24815  divccn  24820  iihalf1cn  24882  iihalf2cn  24885  icchmeo  24894  cnrehmeo  24907  isphtpy  24936  isphtpc  24949  reparphti  24952  pcorevlem  24982  cphnm  25150  tcphnmval  25186  ipcau2  25191  tcphcphlem1  25192  tcphcphlem2  25193  tcphcph  25194  bcthlem1  25281  bcth  25286  mulcncf  25403  dyadmax  25556  volcn  25564  vitalilem1  25566  vitalilem2  25567  vitalilem3  25568  vitali  25571  i1fmullem  25652  itg1addlem4  25657  dvlip  25955  ftc1a  26001  mdegfval  26024  r1pval  26120  coeaddlem  26211  plycn  26223  quotval  26257  elqaalem2  26285  taylfval  26323  psercn2  26389  cxpcn  26711  cxpcn3  26715  resqrtcn  26716  sqrtcn  26717  abscxpbnd  26720  angval  26768  chordthmlem  26799  dcubic  26813  efrlim  26936  lgsdchr  27323  mul2sq  27387  ostthlem2  27596  zaddscl  28339  zmulscld  28342  zseo  28365  tglngval  28535  islnopp  28723  ishpg  28743  finsumvtxdg2size  29535  wspthsn  29835  wwlksnon  29838  wspthsnon  29839  iswspthsnon  29843  2clwwlk  30333  numclwlk1lem2  30356  numclwwlkovh0  30358  hmoval  30796  htth  30904  normval  31110  hlimi  31174  hsn0elch  31234  ocsh  31269  shscli  31303  shs00i  31436  chj00i  31473  riesz4i  32049  stm1addi  32231  stm1add3i  32233  superpos  32340  elrgspnlem2  33243  prmidlc  33468  idlsrgmulrval  33529  brfinext  33699  irngval  33731  minplyval  33744  submateq  33845  metidv  33928  rmulccn  33964  pl1cn  33991  sibfof  34377  cxpcncf1  34632  subfacval2  35214  txsconnlem  35267  cvxpconn  35269  cvxsconn  35270  iscvm  35286  prv  35455  mpomulnzcnf  36322  knoppcnlem10  36525  bj-bary1  37335  ismblfin  37690  itg2addnclem3  37702  itg2addnc  37703  ftc1anclem3  37724  ftc1anc  37730  bfp  37853  rngo2  37936  rngohomco  38003  rngoisoval  38006  rngoisocnv  38010  crngohomfo  38035  keridl  38061  ispridlc  38099  snatpsubN  39774  cdlemn11pre  41234  dihord2pre  41249  baerlem3lem1  41731  sn-inelr  42485  prjcrvfval  42629  mendval  43178  mendplusg  43181  omcl3g  43333  mulvval  44467  fprodcnlem  45608  climf  45631  climf2  45675  cxpcncf2  45908  smflimlem3  46782  fmtnofac2lem  47562  prmdvdsfmtnof1lem2  47579  opoeALTV  47677  opeoALTV  47678  rngchomALTV  48223  funcringcsetcALTV2lem5  48249  ringchomALTV  48257  funcringcsetclem5ALTV  48272  srhmsubcALTVlem2  48279  srhmsubcALTV  48280  fldhmsubcALTV  48288  dmatALTval  48356  lincsumcl  48387  fdivval  48499  catprslem  48965  catprsc  48968  catprsc2  48969  oppcendc  48973  thincmoALT  49295  functhinclem2  49311  fullthinc2  49317  setc1onsubc  49459  lmdfval  49503  cmdfval  49504