Theorem oveq1d 5743

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 5735	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1314  (class class class)co 5728

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-rex 2396  df-v 2659  df-un 3041  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-br 3896  df-iota 5046  df-fv 5089  df-ov 5731

This theorem is referenced by:  fvoveq1d  5750  csbov2g  5766  caovassg  5883  caovdig  5899  caovdirg  5902  caov12d  5906  caov31d  5907  caov411d  5910  grprinvlem  5919  grprinvd  5920  grpridd  5921  caofinvl  5958  omsuc  6322  nnmsucr  6338  nnm1  6374  nnm2  6375  ecovass  6492  ecoviass  6493  ecovdi  6494  ecovidi  6495  addasspig  7086  mulasspig  7088  mulpipq2  7127  distrnqg  7143  ltsonq  7154  ltanqg  7156  ltmnqg  7157  ltexnqq  7164  archnqq  7173  prarloclemarch2  7175  enq0sym  7188  addnq0mo  7203  mulnq0mo  7204  addnnnq0  7205  nqpnq0nq  7209  nq0m0r  7212  nq0a0  7213  nnanq0  7214  distrnq0  7215  addassnq0  7218  addpinq1  7220  prarloclemlo  7250  prarloclem3  7253  prarloclem5  7256  prarloclemcalc  7258  addnqprllem  7283  addnqprulem  7284  appdivnq  7319  recexprlem1ssl  7389  recexprlem1ssu  7390  ltmprr  7398  cauappcvgprlemladdru  7412  cauappcvgprlem1  7415  caucvgprlemnkj  7422  caucvgprlemnbj  7423  caucvgprlemcl  7432  caucvgprlemladdfu  7433  caucvgprlemladdrl  7434  caucvgprlem1  7435  caucvgprprlemcbv  7443  caucvgprprlemval  7444  caucvgprprlemexb  7463  caucvgprprlem1  7465  addcmpblnr  7482  mulcmpblnrlemg  7483  addsrmo  7486  mulsrmo  7487  addsrpr  7488  mulsrpr  7489  ltsrprg  7490  1idsr  7511  pn0sr  7514  recexgt0sr  7516  mulgt0sr  7520  srpospr  7525  prsradd  7528  caucvgsrlemfv  7533  caucvgsrlemcau  7535  caucvgsrlemgt1  7537  caucvgsrlemoffval  7538  caucvgsrlemoffcau  7540  caucvgsrlemoffres  7542  caucvgsrlembnd  7543  caucvgsr  7544  pitonnlem1p1  7581  pitonnlem2  7582  pitonn  7583  recidpirqlemcalc  7592  ax1rid  7612  axrnegex  7614  axcnre  7616  recriota  7625  nntopi  7629  axcaucvglemval  7632  axcaucvglemcau  7633  axcaucvglemres  7634  mul12  7814  mul4  7817  muladd11  7818  readdcan  7825  muladd11r  7841  add12  7843  cnegex  7863  addcan  7865  negeu  7876  pncan2  7892  addsubass  7895  addsub  7896  2addsub  7899  addsubeq4  7900  subid  7904  subid1  7905  npncan  7906  nppcan  7907  nnpcan  7908  nnncan1  7921  npncan3  7923  pnpcan  7924  pnncan  7926  ppncan  7927  addsub4  7928  negsub  7933  subneg  7934  mvlraddd  8048  mvrraddd  8049  subaddeqd  8050  ine0  8075  mulneg1  8076  ltadd2  8100  apreap  8267  cru  8282  recexap  8327  mulcanapd  8335  div23ap  8364  div13ap  8366  divmulassap  8368  divmulasscomap  8369  divcanap4  8372  muldivdirap  8380  divsubdirap  8381  divmuldivap  8385  divdivdivap  8386  divcanap5  8387  divmul13ap  8388  divmuleqap  8390  divdiv32ap  8393  divcanap7  8394  dmdcanap  8395  divdivap1  8396  divdivap2  8397  divadddivap  8400  divsubdivap  8401  conjmulap  8402  divneg2ap  8409  mvllmulapd  8511  lt2mul2div  8547  nndivtr  8672  2halves  8853  halfaddsub  8858  avgle1  8864  avgle2  8865  div4p1lem1div2  8877  un0addcl  8914  un0mulcl  8915  peano2z  8994  zneo  9056  nneoor  9057  nneo  9058  zeo  9060  zeo2  9061  deceq1  9090  qreccl  9336  xaddcom  9537  xnegdi  9544  xaddass  9545  xaddass2  9546  xpncan  9547  xleadd1a  9549  xltadd1  9552  xposdif  9558  xadd4d  9561  lincmb01cmp  9679  iccf1o  9680  fzosubel3  9866  qavgle  9929  2tnp1ge0ge0  9967  fldiv4p1lem1div2  9971  ceilqm1lt  9978  flqdiv  9987  modqlt  9999  modqdiffl  10001  modqcyc2  10026  modqaddabs  10028  mulqaddmodid  10030  mulp1mod1  10031  modqmuladd  10032  modqmuladdnn0  10034  qnegmod  10035  addmodid  10038  addmodidr  10039  modqadd2mod  10040  modqm1p1mod0  10041  modqmul12d  10044  modqnegd  10045  modqadd12d  10046  modqsub12d  10047  q2submod  10051  modqmulmodr  10056  modqaddmulmod  10057  modqsubdir  10059  modfzo0difsn  10061  modsumfzodifsn  10062  addmodlteq  10064  frecuzrdgsuc  10080  frecfzennn  10092  iseqovex  10122  seq3-1p  10146  seq3caopr2  10148  seq3caopr  10149  seq3id  10174  seq3homo  10176  seq3z  10177  expp1  10193  exprecap  10227  expaddzaplem  10229  expmulzap  10232  expdivap  10237  sqval  10244  sqsubswap  10246  subsq  10292  subsq2  10293  binom2  10296  binom2sub  10298  mulbinom2  10301  binom3  10302  zesq  10303  bernneq2  10306  sqoddm1div8  10337  nn0opthlem1d  10359  nn0opthd  10361  nn0opth2d  10362  facp1  10369  facdiv  10377  facndiv  10378  faclbnd  10380  faclbnd2  10381  faclbnd3  10382  bcval  10388  bccmpl  10393  bcm1k  10399  bcp1n  10400  bcp1nk  10401  bcval5  10402  bcp1m1  10404  bcpasc  10405  bcn2m1  10408  hashprg  10447  hashdifpr  10459  hashfzo  10461  hashfzp1  10463  hashfz0  10464  hashxp  10465  zfz1isolemsplit  10474  zfz1isolem1  10476  seq3coll  10478  reval  10514  crre  10522  remim  10525  remul2  10538  immul2  10545  imval2  10559  cjdivap  10574  caucvgre  10645  cvg1nlemcau  10648  cvg1nlemres  10649  resqrexlemp1rp  10670  resqrexlemfp1  10673  resqrexlemover  10674  resqrexlemcalc1  10678  resqrexlemcalc3  10680  resqrexlemnm  10682  resqrexlemoverl  10685  resqrexlemglsq  10686  resqrexlemga  10687  resqrexlemsqa  10688  resqrexlemex  10689  resqrex  10690  sqrtdiv  10706  absvalsq  10717  absreimsq  10731  absdivap  10734  cau3lem  10778  maxabslemlub  10871  maxabslemval  10872  max0addsup  10883  minabs  10899  bdtrilem  10902  bdtri  10903  xrmaxaddlem  10921  xrmaxadd  10922  xrbdtri  10937  clim  10942  clim2  10944  climshftlemg  10963  climshft2  10967  climcn1  10969  climcn2  10970  subcn2  10972  reccn2ap  10974  climmulc2  10992  climsubc2  10994  clim2ser  10998  iser3shft  11007  climcau  11008  serf0  11013  fzosump1  11078  fsum1p  11079  fsump1  11081  sumsplitdc  11093  fsump1i  11094  mptfzshft  11103  fisum0diag2  11108  fsumconst  11115  fsumdifsnconst  11116  modfsummodlemstep  11118  modfsummod  11119  telfsumo  11127  fsumparts  11131  fsumrelem  11132  hash2iun1dif1  11141  binomlem  11144  binom  11145  binom1p  11146  binom1dif  11148  bcxmas  11150  isumsplit  11152  isum1p  11153  arisum  11159  arisum2  11160  trireciplem  11161  geoserap  11168  geolim  11172  geolim2  11173  georeclim  11174  geo2sum  11175  geoisum1  11180  cvgratnnlemseq  11187  cvgratnnlemsumlt  11189  cvgratnnlemfm  11190  cvgratz  11193  mertenslemi1  11196  mertenslem2  11197  mertensabs  11198  efcllemp  11215  ef0lem  11217  efval  11218  esum  11219  ege2le3  11228  efaddlem  11231  efsep  11248  effsumlt  11249  eft0val  11250  efgt1p2  11252  efgt1p  11253  sinval  11260  cosval  11261  resinval  11273  recosval  11274  efi4p  11275  resin4p  11276  recos4p  11277  sinneg  11284  cosneg  11285  efival  11290  sinadd  11294  cosadd  11295  tanaddap  11297  sinmul  11302  cosmul  11303  cos2t  11308  cos2tsin  11309  ef01bndlem  11314  absefib  11327  demoivre  11329  demoivreALT  11330  eirraplem  11331  moddvds  11350  mulmoddvds  11409  3dvds2dec  11411  zeo3  11413  odd2np1lem  11417  odd2np1  11418  oexpneg  11422  2tp1odd  11429  ltoddhalfle  11438  opoe  11440  opeo  11442  omeo  11443  m1expo  11445  m1exp1  11446  nn0o1gt2  11450  nn0o  11452  divalglemnn  11463  divalglemqt  11464  divalglemeunn  11466  divalglemex  11467  divalglemeuneg  11468  flodddiv4  11479  flodddiv4t2lthalf  11482  gcdaddm  11520  bezoutlemnewy  11530  bezoutlema  11533  bezoutlemb  11534  bezoutlemex  11535  bezoutlemaz  11537  mulgcd  11550  gcddiv  11553  gcdmultiplez  11555  rpmulgcd  11560  rplpwr  11561  lcmgcdlem  11604  lcmgcd  11605  divgcdcoprmex  11629  cncongr2  11631  prmexpb  11675  rpexp  11677  rpexp1i  11678  sqrt2irrlem  11685  oddpwdclemxy  11692  oddpwdclemndvds  11694  sqpweven  11698  2sqpwodd  11699  sqne2sq  11700  qmuldeneqnum  11718  nn0gcdsq  11723  zgcdsq  11724  numdensq  11725  dfphi2  11741  phiprmpw  11743  phiprm  11744  hashgcdlem  11748  ennnfonelemkh  11770  ennnfonelemhf1o  11771  resttop  12182  restco  12186  restin  12188  lmfval  12204  cnprcl2k  12217  txrest  12287  txdis1cn  12289  cnmpt2res  12308  psmettri2  12317  psmettri  12319  xmettri2  12350  xmettri  12361  mettri  12362  metrtri  12366  blvalps  12377  blval  12378  xblss2  12394  blhalf  12397  comet  12488  xmetxp  12496  txmetcnp  12507  cnmet  12519  ioo2bl  12529  limcmpted  12588  limcimolemlt  12589  cnplimclemr  12594  limccnp2cntop  12602  reldvg  12603  dvfvalap  12605  dvidlemap  12615  dvconst  12616  dvcnp2cntop  12618  dvaddxxbr  12620  dvmulxxbr  12621  trilpolemeq1  12925  trilpolemlt1  12926