Theorem oveq1d 5890

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveq1d	⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Proof of Theorem oveq1d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq1 5882	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1353  (class class class)co 5875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878

This theorem is referenced by:  fvoveq1d  5897  csbov2g  5916  caovassg  6033  caovdig  6049  caovdirg  6052  caov12d  6056  caov31d  6057  caov411d  6060  caofinvl  6105  omsuc  6473  nnmsucr  6489  nnm1  6526  nnm2  6527  ecovass  6644  ecoviass  6645  ecovdi  6646  ecovidi  6647  addasspig  7329  mulasspig  7331  mulpipq2  7370  distrnqg  7386  ltsonq  7397  ltanqg  7399  ltmnqg  7400  ltexnqq  7407  archnqq  7416  prarloclemarch2  7418  enq0sym  7431  addnq0mo  7446  mulnq0mo  7447  addnnnq0  7448  nqpnq0nq  7452  nq0m0r  7455  nq0a0  7456  nnanq0  7457  distrnq0  7458  addassnq0  7461  addpinq1  7463  prarloclemlo  7493  prarloclem3  7496  prarloclem5  7499  prarloclemcalc  7501  addnqprllem  7526  addnqprulem  7527  appdivnq  7562  recexprlem1ssl  7632  recexprlem1ssu  7633  ltmprr  7641  cauappcvgprlemladdru  7655  cauappcvgprlem1  7658  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemcl  7675  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  caucvgprlem1  7678  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemexb  7706  caucvgprprlem1  7708  addcmpblnr  7738  mulcmpblnrlemg  7739  addsrmo  7742  mulsrmo  7743  addsrpr  7744  mulsrpr  7745  ltsrprg  7746  1idsr  7767  pn0sr  7770  recexgt0sr  7772  mulgt0sr  7777  srpospr  7782  prsradd  7785  caucvgsrlemfv  7790  caucvgsrlemcau  7792  caucvgsrlemgt1  7794  caucvgsrlemoffval  7795  caucvgsrlemoffcau  7797  caucvgsrlemoffres  7799  caucvgsrlembnd  7800  caucvgsr  7801  map2psrprg  7804  pitonnlem1p1  7845  pitonnlem2  7846  pitonn  7847  recidpirqlemcalc  7856  ax1rid  7876  axrnegex  7878  axcnre  7880  recriota  7889  nntopi  7893  axcaucvglemval  7896  axcaucvglemcau  7897  axcaucvglemres  7898  mul12  8086  mul4  8089  muladd11  8090  readdcan  8097  muladd11r  8113  add12  8115  cnegex  8135  addcan  8137  negeu  8148  pncan2  8164  addsubass  8167  addsub  8168  2addsub  8171  addsubeq4  8172  subid  8176  subid1  8177  npncan  8178  nppcan  8179  nnpcan  8180  nnncan1  8193  npncan3  8195  pnpcan  8196  pnncan  8198  ppncan  8199  addsub4  8200  negsub  8205  subneg  8206  subeqxfrd  8320  mvlraddd  8321  mvlladdd  8322  mvrraddd  8323  subaddeqd  8326  ine0  8351  mulneg1  8352  ltadd2  8376  apreap  8544  cru  8559  recexap  8610  mulcanapd  8618  div23ap  8648  div13ap  8650  divmulassap  8652  divmulasscomap  8653  divcanap4  8656  muldivdirap  8664  divsubdirap  8665  divmuldivap  8669  divdivdivap  8670  divcanap5  8671  divmul13ap  8672  divmuleqap  8674  divdiv32ap  8677  divcanap7  8678  dmdcanap  8679  divdivap1  8680  divdivap2  8681  divadddivap  8684  divsubdivap  8685  conjmulap  8686  divneg2ap  8693  subrecap  8796  mvllmulapd  8799  lt2mul2div  8836  nndivtr  8961  2halves  9148  halfaddsub  9153  avgle1  9159  avgle2  9160  div4p1lem1div2  9172  un0addcl  9209  un0mulcl  9210  peano2z  9289  zneo  9354  nneoor  9355  nneo  9356  zeo  9358  zeo2  9359  deceq1  9388  qreccl  9642  xaddcom  9861  xnegdi  9868  xaddass  9869  xaddass2  9870  xpncan  9871  xleadd1a  9873  xltadd1  9876  xposdif  9882  xadd4d  9885  lincmb01cmp  10003  iccf1o  10004  fz0to4untppr  10124  fzosubel3  10196  qavgle  10259  2tnp1ge0ge0  10301  fldiv4p1lem1div2  10305  ceilqm1lt  10312  flqdiv  10321  modqlt  10333  modqdiffl  10335  modqcyc2  10360  modqaddabs  10362  mulqaddmodid  10364  mulp1mod1  10365  modqmuladd  10366  modqmuladdnn0  10368  qnegmod  10369  addmodid  10372  addmodidr  10373  modqadd2mod  10374  modqm1p1mod0  10375  modqmul12d  10378  modqnegd  10379  modqadd12d  10380  modqsub12d  10381  q2submod  10385  modqmulmodr  10390  modqaddmulmod  10391  modqsubdir  10393  modfzo0difsn  10395  modsumfzodifsn  10396  addmodlteq  10398  frecuzrdgsuc  10414  frecfzennn  10426  iseqovex  10456  seq3-1p  10480  seq3caopr2  10482  seq3caopr  10483  seq3id  10508  seq3homo  10510  seq3z  10511  expp1  10527  exprecap  10561  expaddzaplem  10563  expmulzap  10566  expdivap  10571  sqval  10578  sqsubswap  10580  sqdividap  10585  subsq  10627  subsq2  10628  binom2  10632  binom2sub  10634  mulbinom2  10637  binom3  10638  zesq  10639  bernneq2  10642  modqexp  10647  sqoddm1div8  10674  mulsubdivbinom2ap  10691  nn0opthlem1d  10700  nn0opthd  10702  nn0opth2d  10703  facp1  10710  facdiv  10718  facndiv  10719  faclbnd  10721  faclbnd2  10722  faclbnd3  10723  bcval  10729  bccmpl  10734  bcm1k  10740  bcp1n  10741  bcp1nk  10742  bcval5  10743  bcp1m1  10745  bcpasc  10746  bcn2m1  10749  hashprg  10788  hashdifpr  10800  hashfzo  10802  hashfzp1  10804  hashfz0  10805  hashxp  10806  zfz1isolemsplit  10818  zfz1isolem1  10820  seq3coll  10822  reval  10858  crre  10866  remim  10869  remul2  10882  immul2  10889  imval2  10903  cjdivap  10918  caucvgre  10990  cvg1nlemcau  10993  cvg1nlemres  10994  resqrexlemp1rp  11015  resqrexlemfp1  11018  resqrexlemover  11019  resqrexlemcalc1  11023  resqrexlemcalc3  11025  resqrexlemnm  11027  resqrexlemoverl  11030  resqrexlemglsq  11031  resqrexlemga  11032  resqrexlemsqa  11033  resqrexlemex  11034  resqrex  11035  sqrtdiv  11051  absvalsq  11062  absreimsq  11076  absdivap  11079  cau3lem  11123  maxabslemlub  11216  maxabslemval  11217  max0addsup  11228  minabs  11244  bdtrilem  11247  bdtri  11248  xrmaxaddlem  11268  xrmaxadd  11269  xrbdtri  11284  clim  11289  clim2  11291  climshftlemg  11310  climshft2  11314  climcn1  11316  climcn2  11317  subcn2  11319  reccn2ap  11321  climmulc2  11339  climsubc2  11341  clim2ser  11345  iser3shft  11354  climcau  11355  serf0  11360  fzosump1  11425  fsum1p  11426  fsump1  11428  sumsplitdc  11440  fsump1i  11441  mptfzshft  11450  fisum0diag2  11455  fsumconst  11462  fsumdifsnconst  11463  modfsummodlemstep  11465  modfsummod  11466  telfsumo  11474  fsumparts  11478  fsumrelem  11479  hash2iun1dif1  11488  binomlem  11491  binom  11492  binom1p  11493  binom1dif  11495  bcxmas  11497  isumsplit  11499  isum1p  11500  arisum  11506  arisum2  11507  trireciplem  11508  geoserap  11515  geolim  11519  geolim2  11520  georeclim  11521  geo2sum  11522  geoisum1  11527  cvgratnnlemseq  11534  cvgratnnlemsumlt  11536  cvgratnnlemfm  11537  cvgratz  11540  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  fprod1p  11607  fprodp1  11608  fprodcl2lem  11613  fprodfac  11623  fprodeq0  11625  fprodconst  11628  fprodrec  11637  fprodsplit1f  11642  fprodmodd  11649  efcllemp  11666  ef0lem  11668  efval  11669  esum  11670  ege2le3  11679  efaddlem  11682  efsep  11699  effsumlt  11700  eft0val  11701  efgt1p2  11703  efgt1p  11704  sinval  11710  cosval  11711  resinval  11723  recosval  11724  efi4p  11725  resin4p  11726  recos4p  11727  sinneg  11734  cosneg  11735  efival  11740  sinadd  11744  cosadd  11745  tanaddap  11747  sinmul  11752  cosmul  11753  cos2t  11758  cos2tsin  11759  ef01bndlem  11764  absefib  11778  demoivre  11780  demoivreALT  11781  eirraplem  11784  p1modz1  11801  dvdsmodexp  11802  moddvds  11806  mulmoddvds  11869  3dvds2dec  11871  zeo3  11873  odd2np1lem  11877  odd2np1  11878  oexpneg  11882  2tp1odd  11889  ltoddhalfle  11898  opoe  11900  opeo  11902  omeo  11903  m1expo  11905  m1exp1  11906  nn0o1gt2  11910  nn0o  11912  divalglemnn  11923  divalglemqt  11924  divalglemeunn  11926  divalglemex  11927  divalglemeuneg  11928  flodddiv4  11939  flodddiv4t2lthalf  11942  gcdaddm  11985  bezoutlemnewy  11997  bezoutlema  12000  bezoutlemb  12001  bezoutlemex  12002  bezoutlemaz  12004  mulgcd  12017  gcddiv  12020  gcdmultiplez  12022  rpmulgcd  12027  rplpwr  12028  uzwodc  12038  lcmgcdlem  12077  lcmgcd  12078  divgcdcoprmex  12102  cncongr2  12104  prmexpb  12151  rpexp  12153  rpexp1i  12154  sqrt2irrlem  12161  oddpwdclemxy  12169  oddpwdclemndvds  12171  sqpweven  12175  2sqpwodd  12176  sqne2sq  12177  qmuldeneqnum  12195  nn0gcdsq  12200  zgcdsq  12201  numdensq  12202  dfphi2  12220  phiprmpw  12222  phiprm  12223  eulerthlema  12230  eulerthlemh  12231  eulerthlemth  12232  fermltl  12234  prmdiv  12235  prmdiveq  12236  prmdivdiv  12237  hashgcdlem  12238  odzval  12241  odzcllem  12242  odzdvds  12245  vfermltl  12251  powm2modprm  12252  reumodprminv  12253  modprm0  12254  nnnn0modprm0  12255  modprmn0modprm0  12256  coprimeprodsq  12257  coprimeprodsq2  12258  pythagtriplem1  12265  pythagtriplem3  12267  pythagtriplem4  12268  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem15  12278  pythagtriplem16  12279  pythagtriplem17  12280  pythagtriplem18  12281  pceu  12295  pczpre  12297  pcdiv  12302  pcqdiv  12307  pcrec  12308  pczndvds  12315  pcneg  12324  pc2dvds  12329  pcprmpw2  12332  pcaddlem  12338  pcadd  12339  fldivp1  12346  pockthlem  12354  pockthi  12356  4sqlem5  12380  4sqlem9  12384  4sqlem10  12385  4sqlem2  12387  4sqlem3  12388  4sqlem4  12390  mul4sqlem  12391  ennnfonelemkh  12413  ennnfonelemhf1o  12414  setscomd  12503  ressressg  12534  qusin  12746  grprinvlem  12804  grprinvd  12805  grpridd  12806  isnsgrp  12812  sgrpass  12814  sgrp1  12816  mnd12g  12829  mndpropd  12841  mhmlin  12858  grprcan  12910  grpinvid1  12924  isgrpinv  12926  grplcan  12932  grpasscan1  12933  grplmulf1o  12944  grpinvadd  12948  grpinvsub  12952  grpsubsub4  12963  grppnpcan2  12964  grpnpncan  12965  dfgrp3mlem  12968  dfgrp3m  12969  grplactcnv  12972  mhmlem  12978  mhmid  12979  mhmmnd  12980  mulgnnp1  12991  mulg2  12992  mulgnn0p1  12994  mulgsubcl  12997  mulgneg  13001  mulgaddcomlem  13006  mulgaddcom  13007  mulgz  13011  mulgnn0dir  13013  mulgdirlem  13014  mulgdir  13015  mulgneg2  13017  mulgnnass  13018  mulgnn0ass  13019  mulgass  13020  mulgassr  13021  mulgmodid  13022  mulgsubdir  13023  isnsg3  13067  nmzsubg  13070  ssnmz  13071  0nsg  13074  eqger  13083  eqgid  13085  eqgcpbl  13087  ablsub2inv  13114  abladdsub4  13117  abladdsub  13118  ablpncan2  13119  ablpnpcan  13123  ablnncan  13124  ablnnncan1  13127  mgpress  13141  srgass  13154  srgmulgass  13172  srgpcomp  13173  srgpcompp  13174  srgpcomppsc  13175  ringpropd  13217  ringlz  13222  ring1eq0  13225  ringnegl  13228  ringmneg1  13230  ringsubdir  13234  mulgass2  13235  ring1  13236  opprring  13249  unitgrp  13285  dvrcan1  13309  rdivmuldivd  13313  subrginv  13358  islmod  13381  lmodlema  13382  islmodd  13383  lmod0vs  13411  lmodvs0  13412  lmodvsmmulgdi  13413  lmodvneg1  13420  lmodvsneg  13421  lmodsubvs  13433  lmodsubdi  13434  lmodsubdir  13435  lmodprop2d  13438  rmodislmodlem  13440  rmodislmod  13441  resttop  13673  restco  13677  restin  13679  lmfval  13695  cnprcl2k  13709  txrest  13779  txdis1cn  13781  cnmpt2res  13800  psmettri2  13831  psmettri  13833  xmettri2  13864  xmettri  13875  mettri  13876  metrtri  13880  blvalps  13891  blval  13892  xblss2  13908  blhalf  13911  comet  14002  xmetxp  14010  txmetcnp  14021  cnmet  14033  ioo2bl  14046  limcmpted  14135  limcimolemlt  14136  cnplimclemr  14141  limccnp2cntop  14149  reldvg  14151  dvfvalap  14153  dvidlemap  14163  dvconst  14164  dvcnp2cntop  14166  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174  dvcjbr  14175  dvexp  14178  dvrecap  14180  dvmptcmulcn  14186  dveflem  14190  sin0pilem1  14205  sinperlem  14232  ptolemy  14248  tangtx  14262  abssinper  14270  reexplog  14295  relogexp  14296  cxprec  14334  rpdivcxp  14335  cxpmul  14336  rpabscxpbnd  14362  rplogbval  14366  rplogbreexp  14374  rprelogbmul  14376  logbrec  14381  logbgcd1irraplemap  14390  binom4  14400  lgslem1  14404  lgslem4  14407  lgsval  14408  lgsfvalg  14409  lgsval2lem  14414  lgsval4lem  14415  lgsvalmod  14423  lgsneg  14428  lgsneg1  14429  lgsmod  14430  lgsdilem  14431  lgsdir2lem4  14435  lgsdir2  14437  lgsdirprm  14438  lgsdir  14439  lgsne0  14442  lgssq  14444  lgssq2  14445  lgsmulsqcoprm  14450  lgsdirnn0  14451  lgsdinn0  14452  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2lgsoddprmlem1  14456  2lgsoddprmlem2  14457  2lgsoddprmlem3  14462  2sqlem1  14464  2sqlem2  14465  mul2sq  14466  2sqlem3  14467  2sqlem4  14468  2sqlem8  14473  2sqlem9  14474  2sqlem10  14475  trilpolemeq1  14791  trilpolemlt1  14792  trirec0xor  14796  apdifflemf  14797  apdiff  14799