Theorem oveq1d 5547

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

Syntax hints:   → wi 4   = wceq 1284  (class class class)co 5532

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-iota 4887  df-fv 4930  df-ov 5535

This theorem is referenced by:  csbov2g  5566  caovassg  5679  caovdig  5695  caovdirg  5698  caov12d  5702  caov31d  5703  caov411d  5706  grprinvlem  5715  grprinvd  5716  grpridd  5717  caofinvl  5753  omsuc  6074  nnmsucr  6090  nnm1  6120  nnm2  6121  ecovass  6238  ecoviass  6239  ecovdi  6240  ecovidi  6241  addasspig  6520  mulasspig  6522  mulpipq2  6561  distrnqg  6577  ltsonq  6588  ltanqg  6590  ltmnqg  6591  ltexnqq  6598  archnqq  6607  prarloclemarch2  6609  enq0sym  6622  addnq0mo  6637  mulnq0mo  6638  addnnnq0  6639  nqpnq0nq  6643  nq0m0r  6646  nq0a0  6647  nnanq0  6648  distrnq0  6649  addassnq0  6652  addpinq1  6654  prarloclemlo  6684  prarloclem3  6687  prarloclem5  6690  prarloclemcalc  6692  addnqprllem  6717  addnqprulem  6718  appdivnq  6753  recexprlem1ssl  6823  recexprlem1ssu  6824  ltmprr  6832  cauappcvgprlemladdru  6846  cauappcvgprlem1  6849  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemcl  6866  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlem1  6869  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemexb  6897  caucvgprprlem1  6899  addcmpblnr  6916  mulcmpblnrlemg  6917  addsrmo  6920  mulsrmo  6921  addsrpr  6922  mulsrpr  6923  ltsrprg  6924  1idsr  6945  pn0sr  6948  recexgt0sr  6950  mulgt0sr  6954  srpospr  6959  prsradd  6962  caucvgsrlemfv  6967  caucvgsrlemcau  6969  caucvgsrlemgt1  6971  caucvgsrlemoffval  6972  caucvgsrlemoffcau  6974  caucvgsrlemoffres  6976  caucvgsrlembnd  6977  caucvgsr  6978  pitonnlem1p1  7014  pitonnlem2  7015  pitonn  7016  recidpirqlemcalc  7025  ax1rid  7043  axrnegex  7045  axcnre  7047  recriota  7056  nntopi  7060  axcaucvglemval  7063  axcaucvglemcau  7064  axcaucvglemres  7065  mul12  7237  mul4  7240  muladd11  7241  readdcan  7248  muladd11r  7264  add12  7266  cnegex  7286  addcan  7288  negeu  7299  pncan2  7315  addsubass  7318  addsub  7319  2addsub  7322  addsubeq4  7323  subid  7327  subid1  7328  npncan  7329  nppcan  7330  nnpcan  7331  nnncan1  7344  npncan3  7346  pnpcan  7347  pnncan  7349  ppncan  7350  addsub4  7351  negsub  7356  subneg  7357  mvlraddd  7471  mvrraddd  7472  subaddeqd  7473  ine0  7498  mulneg1  7499  ltadd2  7523  apreap  7687  cru  7702  recexap  7743  mulcanapd  7751  div23ap  7779  div13ap  7781  divmulassap  7783  divmulasscomap  7784  divcanap4  7787  muldivdirap  7795  divsubdirap  7796  divmuldivap  7800  divdivdivap  7801  divcanap5  7802  divmul13ap  7803  divmuleqap  7805  divdiv32ap  7808  divcanap7  7809  dmdcanap  7810  divdivap1  7811  divdivap2  7812  divadddivap  7815  divsubdivap  7816  conjmulap  7817  divneg2ap  7824  mvllmulapd  7921  lt2mul2div  7957  nndivtr  8080  2halves  8260  halfaddsub  8265  avgle1  8271  avgle2  8272  div4p1lem1div2  8284  un0addcl  8321  un0mulcl  8322  peano2z  8387  zneo  8448  nneoor  8449  nneo  8450  zeo  8452  zeo2  8453  deceq1  8481  qreccl  8727  lincmb01cmp  9025  iccf1o  9026  fzosubel3  9205  qavgle  9267  2tnp1ge0ge0  9303  fldiv4p1lem1div2  9307  ceilqm1lt  9314  flqdiv  9323  modqlt  9335  modqdiffl  9337  modqcyc2  9362  modqaddabs  9364  mulqaddmodid  9366  mulp1mod1  9367  modqmuladd  9368  modqmuladdnn0  9370  qnegmod  9371  addmodid  9374  addmodidr  9375  modqadd2mod  9376  modqm1p1mod0  9377  modqmul12d  9380  modqnegd  9381  modqadd12d  9382  modqsub12d  9383  q2submod  9387  modqmulmodr  9392  modqaddmulmod  9393  modqsubdir  9395  modfzo0difsn  9397  modsumfzodifsn  9398  addmodlteq  9400  frecuzrdgsuc  9417  frecfzennn  9419  iseqovex  9439  iseq1p  9459  iseqcaopr2  9461  iseqcaopr  9462  iseqid  9467  iseqhomo  9468  iseqz  9469  expp1  9483  exprecap  9517  expaddzaplem  9519  expmulzap  9522  expdivap  9527  sqval  9534  sqsubswap  9536  subsq  9581  subsq2  9582  binom2  9585  binom2sub  9587  mulbinom2  9589  binom3  9590  zesq  9591  bernneq2  9594  sqoddm1div8  9625  nn0opthlem1d  9647  nn0opthd  9649  nn0opth2d  9650  facp1  9657  facdiv  9665  facndiv  9666  faclbnd  9668  faclbnd2  9669  faclbnd3  9670  bcval  9676  bccmpl  9681  bcm1k  9687  bcp1n  9688  bcp1nk  9689  ibcval5  9690  bcp1m1  9692  bcpasc  9693  bcn2m1  9696  reval  9736  crre  9744  remim  9747  remul2  9760  immul2  9767  imval2  9781  cjdivap  9796  caucvgre  9867  cvg1nlemcau  9870  cvg1nlemres  9871  resqrexlemp1rp  9892  resqrexlemfp1  9895  resqrexlemover  9896  resqrexlemcalc1  9900  resqrexlemcalc3  9902  resqrexlemnm  9904  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemga  9909  resqrexlemsqa  9910  resqrexlemex  9911  resqrex  9912  sqrtdiv  9928  absvalsq  9939  absreimsq  9953  absdivap  9956  cau3lem  10000  maxabslemlub  10093  maxabslemval  10094  max0addsup  10105  clim  10120  clim2  10122  climshftlemg  10141  climshft2  10145  climcn1  10147  climcn2  10148  subcn2  10150  climmulc2  10169  climsubc2  10171  clim2iser  10175  climcau  10184  serif0  10189  moddvds  10204  mulmoddvds  10263  3dvds2dec  10265  zeo3  10267  odd2np1lem  10271  odd2np1  10272  oexpneg  10276  2tp1odd  10284  ltoddhalfle  10293  opoe  10295  opeo  10297  omeo  10298  m1expo  10300  m1exp1  10301  nn0o1gt2  10305  nn0o  10307  divalglemnn  10318  divalglemqt  10319  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323  flodddiv4  10334  flodddiv4t2lthalf  10337  gcdaddm  10375  bezoutlemnewy  10385  bezoutlema  10388  bezoutlemb  10389  bezoutlemex  10390  bezoutlemaz  10392  mulgcd  10405  gcddiv  10408  gcdmultiplez  10410  rpmulgcd  10415  rplpwr  10416  lcmgcdlem  10459  lcmgcd  10460  divgcdcoprmex  10484  cncongr2  10486  prmexpb  10530  rpexp  10532  rpexp1i  10533  sqrt2irrlem  10540  oddpwdclemxy  10547  oddpwdclemndvds  10549  sqpweven  10553  2sqpwodd  10554  sqne2sq  10555