Theorem oveq1d 6067

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

Hypothesis

Ref	Expression
oveq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
oveq1d	|- ( ph -> ( A F C ) = ( B F C ) )

Proof of Theorem oveq1d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		oveq1 6059	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1398  (class class class)co 6052

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055

This theorem is referenced by:  fvoveq1d  6074  csbov2g  6094  caovassg  6215  caovdig  6231  caovdirg  6234  caov12d  6238  caov31d  6239  caov411d  6242  caofinvl  6294  suppofss1dcl  6466  suppofss2dcl  6467  omsuc  6707  nnmsucr  6723  nnm1  6760  nnm2  6761  ecovass  6880  ecoviass  6881  ecovdi  6882  ecovidi  6883  isacnm  7512  addasspig  7647  mulasspig  7649  mulpipq2  7688  distrnqg  7704  ltsonq  7715  ltanqg  7717  ltmnqg  7718  ltexnqq  7725  archnqq  7734  prarloclemarch2  7736  enq0sym  7749  addnq0mo  7764  mulnq0mo  7765  addnnnq0  7766  nqpnq0nq  7770  nq0m0r  7773  nq0a0  7774  nnanq0  7775  distrnq0  7776  addassnq0  7779  addpinq1  7781  prarloclemlo  7811  prarloclem3  7814  prarloclem5  7817  prarloclemcalc  7819  addnqprllem  7844  addnqprulem  7845  appdivnq  7880  recexprlem1ssl  7950  recexprlem1ssu  7951  ltmprr  7959  cauappcvgprlemladdru  7973  cauappcvgprlem1  7976  caucvgprlemnkj  7983  caucvgprlemnbj  7984  caucvgprlemcl  7993  caucvgprlemladdfu  7994  caucvgprlemladdrl  7995  caucvgprlem1  7996  caucvgprprlemcbv  8004  caucvgprprlemval  8005  caucvgprprlemexb  8024  caucvgprprlem1  8026  addcmpblnr  8056  mulcmpblnrlemg  8057  addsrmo  8060  mulsrmo  8061  addsrpr  8062  mulsrpr  8063  ltsrprg  8064  1idsr  8085  pn0sr  8088  recexgt0sr  8090  mulgt0sr  8095  srpospr  8100  prsradd  8103  caucvgsrlemfv  8108  caucvgsrlemcau  8110  caucvgsrlemgt1  8112  caucvgsrlemoffval  8113  caucvgsrlemoffcau  8115  caucvgsrlemoffres  8117  caucvgsrlembnd  8118  caucvgsr  8119  map2psrprg  8122  pitonnlem1p1  8163  pitonnlem2  8164  pitonn  8165  recidpirqlemcalc  8174  ax1rid  8194  axrnegex  8196  axcnre  8198  recriota  8207  nntopi  8211  axcaucvglemval  8214  axcaucvglemcau  8215  axcaucvglemres  8216  mul12  8404  mul4  8407  muladd11  8408  readdcan  8415  muladd11r  8431  add12  8433  cnegex  8453  addcan  8455  negeu  8466  pncan2  8482  addsubass  8485  addsub  8486  2addsub  8489  addsubeq4  8490  subid  8494  subid1  8495  npncan  8496  nppcan  8497  nnpcan  8498  nnncan1  8511  npncan3  8513  pnpcan  8514  pnncan  8516  ppncan  8517  addsub4  8518  negsub  8523  subneg  8524  subeqxfrd  8638  mvlraddd  8639  mvlladdd  8640  mvrraddd  8641  subaddeqd  8644  ine0  8669  mulneg1  8670  ltadd2  8695  apreap  8863  cru  8878  recexap  8929  mulcanapd  8937  div23ap  8967  div13ap  8969  divmulassap  8971  divmulasscomap  8972  divcanap4  8975  muldivdirap  8983  divsubdirap  8984  divmuldivap  8988  divdivdivap  8989  divcanap5  8990  divmul13ap  8991  divmuleqap  8993  divdiv32ap  8996  divcanap7  8997  dmdcanap  8998  divdivap1  8999  divdivap2  9000  divadddivap  9003  divsubdivap  9004  conjmulap  9005  divneg2ap  9012  subrecap  9115  mvllmulapd  9118  lt2mul2div  9155  nndivtr  9281  2halves  9469  halfaddsub  9474  subhalfhalf  9475  avgle1  9481  avgle2  9482  div4p1lem1div2  9494  un0addcl  9531  un0mulcl  9532  peano2z  9615  zneo  9682  nneoor  9683  nneo  9684  zeo  9686  zeo2  9687  deceq1  9716  qreccl  9977  xaddcom  10197  xnegdi  10204  xaddass  10205  xaddass2  10206  xpncan  10207  xleadd1a  10209  xltadd1  10212  xposdif  10218  xadd4d  10221  lincmb01cmp  10339  lincmble  10340  iccf1o  10341  fzspl  10407  fz0to4untppr  10462  fzo0addel  10537  fzosubel3  10545  qavgle  10622  2tnp1ge0ge0  10665  fldiv4p1lem1div2  10669  fldiv4lem1div2  10671  ceilqm1lt  10678  flqdiv  10687  modqlt  10699  modqdiffl  10701  modqcyc2  10726  modqaddabs  10728  mulqaddmodid  10730  mulp1mod1  10731  modqmuladd  10732  modqmuladdnn0  10734  qnegmod  10735  addmodid  10738  addmodidr  10739  modqadd2mod  10740  modqm1p1mod0  10741  modqmul12d  10744  modqnegd  10745  modqadd12d  10746  modqsub12d  10747  q2submod  10751  modqmulmodr  10756  modqaddmulmod  10757  modqsubdir  10759  modfzo0difsn  10761  modsumfzodifsn  10762  addmodlteq  10764  frecuzrdgsuc  10780  frecfzennn  10792  iseqovex  10824  seq3-1p  10856  seq3caopr2  10859  seqcaopr2g  10860  seq3caopr  10861  seqcaoprg  10862  seqf1oglem2a  10884  seqf1oglem1  10885  seqf1oglem2  10886  seq3id  10891  seq3homo  10893  seq3z  10894  seqhomog  10896  seqfeq4g  10897  expp1  10912  exprecap  10946  expaddzaplem  10948  expmulzap  10951  expdivap  10956  sqval  10963  sqsubswap  10965  sqdividap  10970  subsq  11012  subsq2  11013  binom2  11017  binom2sub  11019  mulbinom2  11022  binom3  11023  zesq  11024  bernneq2  11027  modqexp  11032  sqoddm1div8  11059  mulsubdivbinom2ap  11077  nn0opthlem1d  11086  nn0opthd  11088  nn0opth2d  11089  facp1  11096  facdiv  11104  facndiv  11105  faclbnd  11107  faclbnd2  11108  faclbnd3  11109  bcval  11115  bccmpl  11120  bcm1k  11126  bcp1n  11127  bcp1nk  11128  bcval5  11129  bcp1m1  11131  bcpasc  11132  bcm1n  11135  bcn2m1  11136  hashprg  11177  hashdifpr  11189  hashfzo  11191  hashfzp1  11193  hashfz0  11194  hashxp  11195  hashfibclem  11210  hashfibc  11211  zfz1isolemsplit  11214  zfz1isolem1  11216  seq3coll  11218  lswwrd  11275  ccatfvalfi  11284  ccatass  11300  lswccatn0lsw  11303  wrdlenccats1lenm1g  11328  ccatw2s1leng  11330  ccatswrd  11366  ccatpfx  11397  swrdpfx  11403  pfxpfx  11404  ccats1pfxeq  11410  wrdeqs1cat  11416  wrdind  11418  wrd2ind  11419  pfxccatpfx2  11433  pfxccatin12d  11441  cats1catd  11464  cats2catd  11465  s2leng  11485  s3s4d  11499  s2s5d  11500  s5s2d  11501  reval  11538  crre  11546  remim  11549  remul2  11562  immul2  11569  imval2  11583  cjdivap  11598  caucvgre  11670  cvg1nlemcau  11673  cvg1nlemres  11674  resqrexlemp1rp  11695  resqrexlemfp1  11698  resqrexlemover  11699  resqrexlemcalc1  11703  resqrexlemcalc3  11705  resqrexlemnm  11707  resqrexlemoverl  11710  resqrexlemglsq  11711  resqrexlemga  11712  resqrexlemsqa  11713  resqrexlemex  11714  resqrex  11715  sqrtdiv  11731  absvalsq  11742  absreimsq  11756  absdivap  11759  cau3lem  11803  maxabslemlub  11896  maxabslemval  11897  max0addsup  11908  minabs  11925  bdtrilem  11928  bdtri  11929  xrmaxaddlem  11949  xrmaxadd  11950  xrbdtri  11965  clim  11970  clim2  11972  climshftlemg  11991  climshft2  11995  climcn1  11997  climcn2  11998  subcn2  12000  reccn2ap  12002  climmulc2  12020  climsubc2  12022  clim2ser  12026  iser3shft  12035  climcau  12036  serf0  12041  fzosump1  12107  fsum1p  12108  fsump1  12110  sumsplitdc  12122  fsump1i  12123  mptfzshft  12132  fisum0diag2  12137  fsumconst  12144  fsumdifsnconst  12145  modfsummodlemstep  12147  modfsummod  12148  telfsumo  12156  fsumparts  12160  fsumrelem  12161  hash2iun1dif1  12170  binomlem  12173  binom  12174  binom1p  12175  binom1dif  12177  bcxmas  12179  isumsplit  12181  isum1p  12182  arisum  12188  arisum2  12189  trireciplem  12190  geoserap  12197  geolim  12201  geolim2  12202  georeclim  12203  geo2sum  12204  geoisum1  12209  cvgratnnlemseq  12216  cvgratnnlemsumlt  12218  cvgratnnlemfm  12219  cvgratz  12222  mertenslemi1  12225  mertenslem2  12226  mertensabs  12227  fprod1p  12289  fprodp1  12290  fprodcl2lem  12295  fprodfac  12305  fprodeq0  12307  fprodconst  12310  fprodrec  12319  fprodsplit1f  12324  fprodmodd  12331  efcllemp  12348  ef0lem  12350  efval  12351  esum  12352  ege2le3  12361  efaddlem  12364  efsep  12381  effsumlt  12382  eft0val  12383  efgt1p2  12385  efgt1p  12386  sinval  12392  cosval  12393  resinval  12405  recosval  12406  efi4p  12407  resin4p  12408  recos4p  12409  sinneg  12416  cosneg  12417  efival  12422  sinadd  12426  cosadd  12427  tanaddap  12429  sinmul  12434  cosmul  12435  cos2t  12440  cos2tsin  12441  ef01bndlem  12446  absefib  12461  demoivre  12463  demoivreALT  12464  eirraplem  12467  p1modz1  12484  dvdsmodexp  12485  moddvds  12489  mulmoddvds  12553  3dvds2dec  12556  zeo3  12558  odd2np1lem  12562  odd2np1  12563  oexpneg  12567  2tp1odd  12574  ltoddhalfle  12583  opoe  12585  opeo  12587  omeo  12588  m1expo  12590  m1exp1  12591  nn0o1gt2  12595  nn0o  12597  divalglemnn  12608  divalglemqt  12609  divalglemeunn  12611  divalglemex  12612  divalglemeuneg  12613  flodddiv4  12626  flodddiv4t2lthalf  12629  bitsp1o  12643  bitsmod  12646  bitsinv1lem  12651  gcdaddm  12684  bezoutlemnewy  12696  bezoutlema  12699  bezoutlemb  12700  bezoutlemex  12701  bezoutlemaz  12703  mulgcd  12716  gcddiv  12719  gcdmultiplez  12721  rpmulgcd  12726  rplpwr  12727  uzwodc  12737  lcmgcdlem  12778  lcmgcd  12779  divgcdcoprmex  12803  cncongr2  12805  prmexpb  12852  rpexp  12854  rpexp1i  12855  sqrt2irrlem  12862  oddpwdclemxy  12870  oddpwdclemndvds  12872  sqpweven  12876  2sqpwodd  12877  sqne2sq  12878  qmuldeneqnum  12896  nn0gcdsq  12901  zgcdsq  12902  numdensq  12903  dfphi2  12921  phiprmpw  12923  phiprm  12924  eulerthlema  12931  eulerthlemh  12932  eulerthlemth  12933  fermltl  12935  prmdiv  12936  prmdiveq  12937  prmdivdiv  12938  hashgcdlem  12939  odzval  12943  odzcllem  12944  odzdvds  12947  vfermltl  12953  powm2modprm  12954  reumodprminv  12955  modprm0  12956  nnnn0modprm0  12957  modprmn0modprm0  12958  coprimeprodsq  12959  coprimeprodsq2  12960  pythagtriplem1  12967  pythagtriplem3  12969  pythagtriplem4  12970  pythagtriplem6  12972  pythagtriplem7  12973  pythagtriplem12  12977  pythagtriplem14  12979  pythagtriplem15  12980  pythagtriplem16  12981  pythagtriplem17  12982  pythagtriplem18  12983  pceu  12997  pczpre  12999  pcdiv  13004  pcqdiv  13009  pcrec  13010  pczndvds  13018  pcneg  13027  pc2dvds  13032  pcprmpw2  13035  pcaddlem  13041  pcadd  13042  fldivp1  13050  pockthlem  13058  pockthi  13060  4sqlem5  13084  4sqlem9  13088  4sqlem10  13089  4sqlem2  13091  4sqlem3  13092  4sqlem4  13094  mul4sqlem  13095  4sqlem11  13103  4sqlem12  13104  4sqlem14  13106  4sqlem15  13107  4sqlem17  13109  4sqlem19  13111  ballotfilem2  13149  ballotfilemfp1  13152  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilem4  13159  ennnfonelemkh  13180  ennnfonelemhf1o  13181  setscomd  13270  ressressg  13305  qusex  13555  qusin  13556  grpinvalem  13615  grpinva  13616  grprida  13617  gsumsplit1r  13628  isnsgrp  13636  sgrpass  13638  sgrp1  13641  sgrppropd  13643  prdssgrpd  13645  mnd12g  13658  mndpropd  13670  prdsidlem  13677  prdsmndd  13678  imasmnd2  13682  mhmex  13692  mhmlin  13697  grprcan  13767  grpinvid1  13782  isgrpinv  13784  grplcan  13792  grpasscan1  13793  grplmulf1o  13804  grpinvadd  13808  grpinvsub  13812  grpsubsub4  13823  grppnpcan2  13824  grpnpncan  13825  dfgrp3mlem  13828  dfgrp3m  13829  grplactcnv  13832  prdsinvlem  13838  imasgrp2  13844  mhmlem  13848  mhmid  13849  mhmmnd  13850  mulgnnp1  13864  mulg2  13865  mulgnn0p1  13867  mulgsubcl  13870  mulgneg  13874  mulgaddcomlem  13879  mulgaddcom  13880  mulgz  13884  mulgnn0dir  13886  mulgdirlem  13887  mulgdir  13888  mulgneg2  13890  mulgnnass  13891  mulgnn0ass  13892  mulgass  13893  mulgassr  13894  mulgmodid  13895  mulgsubdir  13896  submmulg  13900  isnsg3  13941  nmzsubg  13944  ssnmz  13945  0nsg  13948  eqger  13958  eqgid  13960  eqgcpbl  13962  ghmlin  13982  ghmmulg  13990  ghmnsgima  14002  ghmnsgpreima  14003  conjghm  14010  conjnmz  14013  ablsub2inv  14045  abladdsub4  14048  abladdsub  14049  ablpncan2  14050  ablpnpcan  14054  ablnncan  14055  ablnnncan1  14058  gsumfzconst  14075  gsumfzsnfd  14079  gsumsplit0  14080  mgpress  14092  rngass  14100  rngdi  14101  rngdir  14102  rnglz  14106  rngmneg1  14108  rngsubdir  14113  rngpropd  14116  imasrng  14117  srgass  14132  srgmulgass  14150  srgpcomp  14151  srgpcompp  14152  srgpcomppsc  14153  ringpropd  14199  ringlz  14204  ring1eq0  14209  ringnegl  14212  ringmneg1  14214  ringsubdir  14218  mulgass2  14219  ring1  14220  imasring  14225  opprrng  14238  opprring  14240  unitgrp  14278  dvrcan1  14302  rdivmuldivd  14306  subrginv  14399  resrhm  14410  unitrrg  14430  aprlring  14451  islmod  14456  lmodlema  14457  islmodd  14458  lmod0vs  14486  lmodvs0  14487  lmodvsmmulgdi  14488  lmodvneg1  14495  lmodvsneg  14496  lmodsubvs  14508  lmodsubdi  14509  lmodsubdir  14510  lmodprop2d  14513  rmodislmodlem  14515  rmodislmod  14516  lsssetm  14521  islssmd  14524  lssclg  14529  lssvacl  14530  lss1d  14548  lsspropdg  14596  sraval  14602  rnglidlmcl  14645  gsumfzfsumlemm  14752  znunit  14824  mplsubgfilemcl  14871  resttop  15052  restco  15056  restin  15058  lmfval  15075  cnprcl2k  15088  txrest  15158  txdis1cn  15160  cnmpt2res  15179  psmettri2  15210  psmettri  15212  xmettri2  15243  xmettri  15254  mettri  15255  metrtri  15259  blvalps  15270  blval  15271  xblss2  15287  blhalf  15290  comet  15381  xmetxp  15389  txmetcnp  15400  cnmet  15412  ioo2bl  15433  ivthreinc  15527  limcmpted  15545  limcimolemlt  15546  cnplimclemr  15551  limccnp2cntop  15559  reldvg  15561  dvfvalap  15563  dvidlemap  15573  dvidrelem  15574  dvidsslem  15575  dvconst  15576  dvconstre  15578  dvconstss  15580  dvcnp2cntop  15581  dvaddxxbr  15583  dvmulxxbr  15584  dvcoapbr  15589  dvcjbr  15590  dvexp  15593  dvrecap  15595  dvmptcmulcn  15603  dveflem  15608  plyval  15614  elply2  15617  elplyr  15622  elplyd  15623  ply1termlem  15624  plyaddlem1  15629  plymullem1  15630  plycoeid3  15639  plycjlemc  15642  dvply1  15647  sin0pilem1  15663  sinperlem  15690  ptolemy  15706  tangtx  15720  abssinper  15728  reexplog  15753  relogexp  15754  cxprec  15792  rpdivcxp  15793  cxpmul  15794  rpabscxpbnd  15822  rplogbval  15827  rplogbreexp  15835  rprelogbmul  15837  logbrec  15842  logbgcd1irraplemap  15851  binom4  15861  pellexlem2  15863  pellexlem3  15864  wilthlem1  15865  mpodvdsmulf1o  15875  sgmppw  15877  0sgmppw  15878  1sgmprm  15879  1sgm2ppw  15880  perfectlem1  15884  perfectlem2  15885  perfect  15886  lgslem1  15890  lgslem4  15893  lgsval  15894  lgsfvalg  15895  lgsval2lem  15900  lgsval4lem  15901  lgsvalmod  15909  lgsneg  15914  lgsneg1  15915  lgsmod  15916  lgsdilem  15917  lgsdir2lem4  15921  lgsdir2  15923  lgsdirprm  15924  lgsdir  15925  lgsne0  15928  lgssq  15930  lgssq2  15931  lgsmulsqcoprm  15936  lgsdirnn0  15937  lgsdinn0  15938  gausslemma2dlem1a  15948  gausslemma2dlem4  15954  gausslemma2dlem5a  15955  gausslemma2dlem5  15956  gausslemma2dlem6  15957  gausslemma2dlem7  15958  gausslemma2d  15959  lgseisenlem1  15960  lgseisenlem2  15961  lgseisenlem3  15962  lgseisenlem4  15963  lgseisen  15964  lgsquadlem1  15967  lgsquadlem2  15968  lgsquad2lem1  15971  lgsquad2lem2  15972  lgsquad3  15974  m1lgs  15975  2lgslem1a  15978  2lgslem1c  15980  2lgslem3a  15983  2lgslem3b  15984  2lgslem3c  15985  2lgslem3d  15986  2lgslem3a1  15987  2lgslem3b1  15988  2lgslem3c1  15989  2lgslem3d1  15990  2lgsoddprmlem1  15995  2lgsoddprmlem2  15996  2lgsoddprmlem3  16001  2sqlem1  16004  2sqlem2  16005  mul2sq  16006  2sqlem3  16007  2sqlem4  16008  2sqlem8  16013  2sqlem9  16014  2sqlem10  16015  vdegp1bid  16327  uspgr2wlkeqi  16379  isclwwlk  16406  clwwlkccatlem  16412  clwwlknonex2  16451  repiecele0  16827  repiecege0  16828  repiecef  16829  trilpolemeq1  16841  trilpolemlt1  16842  trirec0xor  16846  apdifflemf  16847  apdiff  16849  qdiff  16850  gsumgfsumlem  16882  gsumgfsum  16883