Theorem oveq1d 5782

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

Syntax hints:   → wi 4   = wceq 1331  (class class class)co 5767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rex 2420  df-v 2683  df-un 3070  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-br 3925  df-iota 5083  df-fv 5126  df-ov 5770

This theorem is referenced by:  fvoveq1d  5789  csbov2g  5805  caovassg  5922  caovdig  5938  caovdirg  5941  caov12d  5945  caov31d  5946  caov411d  5949  grprinvlem  5958  grprinvd  5959  grpridd  5960  caofinvl  5997  omsuc  6361  nnmsucr  6377  nnm1  6413  nnm2  6414  ecovass  6531  ecoviass  6532  ecovdi  6533  ecovidi  6534  addasspig  7131  mulasspig  7133  mulpipq2  7172  distrnqg  7188  ltsonq  7199  ltanqg  7201  ltmnqg  7202  ltexnqq  7209  archnqq  7218  prarloclemarch2  7220  enq0sym  7233  addnq0mo  7248  mulnq0mo  7249  addnnnq0  7250  nqpnq0nq  7254  nq0m0r  7257  nq0a0  7258  nnanq0  7259  distrnq0  7260  addassnq0  7263  addpinq1  7265  prarloclemlo  7295  prarloclem3  7298  prarloclem5  7301  prarloclemcalc  7303  addnqprllem  7328  addnqprulem  7329  appdivnq  7364  recexprlem1ssl  7434  recexprlem1ssu  7435  ltmprr  7443  cauappcvgprlemladdru  7457  cauappcvgprlem1  7460  caucvgprlemnkj  7467  caucvgprlemnbj  7468  caucvgprlemcl  7477  caucvgprlemladdfu  7478  caucvgprlemladdrl  7479  caucvgprlem1  7480  caucvgprprlemcbv  7488  caucvgprprlemval  7489  caucvgprprlemexb  7508  caucvgprprlem1  7510  addcmpblnr  7540  mulcmpblnrlemg  7541  addsrmo  7544  mulsrmo  7545  addsrpr  7546  mulsrpr  7547  ltsrprg  7548  1idsr  7569  pn0sr  7572  recexgt0sr  7574  mulgt0sr  7579  srpospr  7584  prsradd  7587  caucvgsrlemfv  7592  caucvgsrlemcau  7594  caucvgsrlemgt1  7596  caucvgsrlemoffval  7597  caucvgsrlemoffcau  7599  caucvgsrlemoffres  7601  caucvgsrlembnd  7602  caucvgsr  7603  map2psrprg  7606  pitonnlem1p1  7647  pitonnlem2  7648  pitonn  7649  recidpirqlemcalc  7658  ax1rid  7678  axrnegex  7680  axcnre  7682  recriota  7691  nntopi  7695  axcaucvglemval  7698  axcaucvglemcau  7699  axcaucvglemres  7700  mul12  7884  mul4  7887  muladd11  7888  readdcan  7895  muladd11r  7911  add12  7913  cnegex  7933  addcan  7935  negeu  7946  pncan2  7962  addsubass  7965  addsub  7966  2addsub  7969  addsubeq4  7970  subid  7974  subid1  7975  npncan  7976  nppcan  7977  nnpcan  7978  nnncan1  7991  npncan3  7993  pnpcan  7994  pnncan  7996  ppncan  7997  addsub4  7998  negsub  8003  subneg  8004  subeqxfrd  8118  mvlraddd  8119  mvlladdd  8120  mvrraddd  8121  subaddeqd  8124  ine0  8149  mulneg1  8150  ltadd2  8174  apreap  8342  cru  8357  recexap  8407  mulcanapd  8415  div23ap  8444  div13ap  8446  divmulassap  8448  divmulasscomap  8449  divcanap4  8452  muldivdirap  8460  divsubdirap  8461  divmuldivap  8465  divdivdivap  8466  divcanap5  8467  divmul13ap  8468  divmuleqap  8470  divdiv32ap  8473  divcanap7  8474  dmdcanap  8475  divdivap1  8476  divdivap2  8477  divadddivap  8480  divsubdivap  8481  conjmulap  8482  divneg2ap  8489  subrecap  8591  mvllmulapd  8594  lt2mul2div  8630  nndivtr  8755  2halves  8942  halfaddsub  8947  avgle1  8953  avgle2  8954  div4p1lem1div2  8966  un0addcl  9003  un0mulcl  9004  peano2z  9083  zneo  9145  nneoor  9146  nneo  9147  zeo  9149  zeo2  9150  deceq1  9179  qreccl  9427  xaddcom  9637  xnegdi  9644  xaddass  9645  xaddass2  9646  xpncan  9647  xleadd1a  9649  xltadd1  9652  xposdif  9658  xadd4d  9661  lincmb01cmp  9779  iccf1o  9780  fzosubel3  9966  qavgle  10029  2tnp1ge0ge0  10067  fldiv4p1lem1div2  10071  ceilqm1lt  10078  flqdiv  10087  modqlt  10099  modqdiffl  10101  modqcyc2  10126  modqaddabs  10128  mulqaddmodid  10130  mulp1mod1  10131  modqmuladd  10132  modqmuladdnn0  10134  qnegmod  10135  addmodid  10138  addmodidr  10139  modqadd2mod  10140  modqm1p1mod0  10141  modqmul12d  10144  modqnegd  10145  modqadd12d  10146  modqsub12d  10147  q2submod  10151  modqmulmodr  10156  modqaddmulmod  10157  modqsubdir  10159  modfzo0difsn  10161  modsumfzodifsn  10162  addmodlteq  10164  frecuzrdgsuc  10180  frecfzennn  10192  iseqovex  10222  seq3-1p  10246  seq3caopr2  10248  seq3caopr  10249  seq3id  10274  seq3homo  10276  seq3z  10277  expp1  10293  exprecap  10327  expaddzaplem  10329  expmulzap  10332  expdivap  10337  sqval  10344  sqsubswap  10346  subsq  10392  subsq2  10393  binom2  10396  binom2sub  10398  mulbinom2  10401  binom3  10402  zesq  10403  bernneq2  10406  sqoddm1div8  10437  nn0opthlem1d  10459  nn0opthd  10461  nn0opth2d  10462  facp1  10469  facdiv  10477  facndiv  10478  faclbnd  10480  faclbnd2  10481  faclbnd3  10482  bcval  10488  bccmpl  10493  bcm1k  10499  bcp1n  10500  bcp1nk  10501  bcval5  10502  bcp1m1  10504  bcpasc  10505  bcn2m1  10508  hashprg  10547  hashdifpr  10559  hashfzo  10561  hashfzp1  10563  hashfz0  10564  hashxp  10565  zfz1isolemsplit  10574  zfz1isolem1  10576  seq3coll  10578  reval  10614  crre  10622  remim  10625  remul2  10638  immul2  10645  imval2  10659  cjdivap  10674  caucvgre  10746  cvg1nlemcau  10749  cvg1nlemres  10750  resqrexlemp1rp  10771  resqrexlemfp1  10774  resqrexlemover  10775  resqrexlemcalc1  10779  resqrexlemcalc3  10781  resqrexlemnm  10783  resqrexlemoverl  10786  resqrexlemglsq  10787  resqrexlemga  10788  resqrexlemsqa  10789  resqrexlemex  10790  resqrex  10791  sqrtdiv  10807  absvalsq  10818  absreimsq  10832  absdivap  10835  cau3lem  10879  maxabslemlub  10972  maxabslemval  10973  max0addsup  10984  minabs  11000  bdtrilem  11003  bdtri  11004  xrmaxaddlem  11022  xrmaxadd  11023  xrbdtri  11038  clim  11043  clim2  11045  climshftlemg  11064  climshft2  11068  climcn1  11070  climcn2  11071  subcn2  11073  reccn2ap  11075  climmulc2  11093  climsubc2  11095  clim2ser  11099  iser3shft  11108  climcau  11109  serf0  11114  fzosump1  11179  fsum1p  11180  fsump1  11182  sumsplitdc  11194  fsump1i  11195  mptfzshft  11204  fisum0diag2  11209  fsumconst  11216  fsumdifsnconst  11217  modfsummodlemstep  11219  modfsummod  11220  telfsumo  11228  fsumparts  11232  fsumrelem  11233  hash2iun1dif1  11242  binomlem  11245  binom  11246  binom1p  11247  binom1dif  11249  bcxmas  11251  isumsplit  11253  isum1p  11254  arisum  11260  arisum2  11261  trireciplem  11262  geoserap  11269  geolim  11273  geolim2  11274  georeclim  11275  geo2sum  11276  geoisum1  11281  cvgratnnlemseq  11288  cvgratnnlemsumlt  11290  cvgratnnlemfm  11291  cvgratz  11294  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  efcllemp  11353  ef0lem  11355  efval  11356  esum  11357  ege2le3  11366  efaddlem  11369  efsep  11386  effsumlt  11387  eft0val  11388  efgt1p2  11390  efgt1p  11391  sinval  11398  cosval  11399  resinval  11411  recosval  11412  efi4p  11413  resin4p  11414  recos4p  11415  sinneg  11422  cosneg  11423  efival  11428  sinadd  11432  cosadd  11433  tanaddap  11435  sinmul  11440  cosmul  11441  cos2t  11446  cos2tsin  11447  ef01bndlem  11452  absefib  11466  demoivre  11468  demoivreALT  11469  eirraplem  11472  moddvds  11491  mulmoddvds  11550  3dvds2dec  11552  zeo3  11554  odd2np1lem  11558  odd2np1  11559  oexpneg  11563  2tp1odd  11570  ltoddhalfle  11579  opoe  11581  opeo  11583  omeo  11584  m1expo  11586  m1exp1  11587  nn0o1gt2  11591  nn0o  11593  divalglemnn  11604  divalglemqt  11605  divalglemeunn  11607  divalglemex  11608  divalglemeuneg  11609  flodddiv4  11620  flodddiv4t2lthalf  11623  gcdaddm  11661  bezoutlemnewy  11673  bezoutlema  11676  bezoutlemb  11677  bezoutlemex  11678  bezoutlemaz  11680  mulgcd  11693  gcddiv  11696  gcdmultiplez  11698  rpmulgcd  11703  rplpwr  11704  lcmgcdlem  11747  lcmgcd  11748  divgcdcoprmex  11772  cncongr2  11774  prmexpb  11818  rpexp  11820  rpexp1i  11821  sqrt2irrlem  11828  oddpwdclemxy  11836  oddpwdclemndvds  11838  sqpweven  11842  2sqpwodd  11843  sqne2sq  11844  qmuldeneqnum  11862  nn0gcdsq  11867  zgcdsq  11868  numdensq  11869  dfphi2  11885  phiprmpw  11887  phiprm  11888  hashgcdlem  11892  ennnfonelemkh  11914  ennnfonelemhf1o  11915  resttop  12328  restco  12332  restin  12334  lmfval  12350  cnprcl2k  12364  txrest  12434  txdis1cn  12436  cnmpt2res  12455  psmettri2  12486  psmettri  12488  xmettri2  12519  xmettri  12530  mettri  12531  metrtri  12535  blvalps  12546  blval  12547  xblss2  12563  blhalf  12566  comet  12657  xmetxp  12665  txmetcnp  12676  cnmet  12688  ioo2bl  12701  limcmpted  12790  limcimolemlt  12791  cnplimclemr  12796  limccnp2cntop  12804  reldvg  12806  dvfvalap  12808  dvidlemap  12818  dvconst  12819  dvcnp2cntop  12821  dvaddxxbr  12823  dvmulxxbr  12824  dvcoapbr  12829  dvcjbr  12830  dvexp  12833  dvrecap  12835  dvmptcmulcn  12841  dveflem  12844  sin0pilem1  12851  sinperlem  12878  ptolemy  12894  tangtx  12908  abssinper  12916  trilpolemeq1  13222  trilpolemlt1  13223