Theorem oveq1d 5903

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 5895	. 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 1363  (class class class)co 5888

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rex 2471  df-v 2751  df-un 3145  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-iota 5190  df-fv 5236  df-ov 5891

This theorem is referenced by:  fvoveq1d  5910  csbov2g  5929  caovassg  6047  caovdig  6063  caovdirg  6066  caov12d  6070  caov31d  6071  caov411d  6074  caofinvl  6119  omsuc  6487  nnmsucr  6503  nnm1  6540  nnm2  6541  ecovass  6658  ecoviass  6659  ecovdi  6660  ecovidi  6661  addasspig  7343  mulasspig  7345  mulpipq2  7384  distrnqg  7400  ltsonq  7411  ltanqg  7413  ltmnqg  7414  ltexnqq  7421  archnqq  7430  prarloclemarch2  7432  enq0sym  7445  addnq0mo  7460  mulnq0mo  7461  addnnnq0  7462  nqpnq0nq  7466  nq0m0r  7469  nq0a0  7470  nnanq0  7471  distrnq0  7472  addassnq0  7475  addpinq1  7477  prarloclemlo  7507  prarloclem3  7510  prarloclem5  7513  prarloclemcalc  7515  addnqprllem  7540  addnqprulem  7541  appdivnq  7576  recexprlem1ssl  7646  recexprlem1ssu  7647  ltmprr  7655  cauappcvgprlemladdru  7669  cauappcvgprlem1  7672  caucvgprlemnkj  7679  caucvgprlemnbj  7680  caucvgprlemcl  7689  caucvgprlemladdfu  7690  caucvgprlemladdrl  7691  caucvgprlem1  7692  caucvgprprlemcbv  7700  caucvgprprlemval  7701  caucvgprprlemexb  7720  caucvgprprlem1  7722  addcmpblnr  7752  mulcmpblnrlemg  7753  addsrmo  7756  mulsrmo  7757  addsrpr  7758  mulsrpr  7759  ltsrprg  7760  1idsr  7781  pn0sr  7784  recexgt0sr  7786  mulgt0sr  7791  srpospr  7796  prsradd  7799  caucvgsrlemfv  7804  caucvgsrlemcau  7806  caucvgsrlemgt1  7808  caucvgsrlemoffval  7809  caucvgsrlemoffcau  7811  caucvgsrlemoffres  7813  caucvgsrlembnd  7814  caucvgsr  7815  map2psrprg  7818  pitonnlem1p1  7859  pitonnlem2  7860  pitonn  7861  recidpirqlemcalc  7870  ax1rid  7890  axrnegex  7892  axcnre  7894  recriota  7903  nntopi  7907  axcaucvglemval  7910  axcaucvglemcau  7911  axcaucvglemres  7912  mul12  8100  mul4  8103  muladd11  8104  readdcan  8111  muladd11r  8127  add12  8129  cnegex  8149  addcan  8151  negeu  8162  pncan2  8178  addsubass  8181  addsub  8182  2addsub  8185  addsubeq4  8186  subid  8190  subid1  8191  npncan  8192  nppcan  8193  nnpcan  8194  nnncan1  8207  npncan3  8209  pnpcan  8210  pnncan  8212  ppncan  8213  addsub4  8214  negsub  8219  subneg  8220  subeqxfrd  8334  mvlraddd  8335  mvlladdd  8336  mvrraddd  8337  subaddeqd  8340  ine0  8365  mulneg1  8366  ltadd2  8390  apreap  8558  cru  8573  recexap  8624  mulcanapd  8632  div23ap  8662  div13ap  8664  divmulassap  8666  divmulasscomap  8667  divcanap4  8670  muldivdirap  8678  divsubdirap  8679  divmuldivap  8683  divdivdivap  8684  divcanap5  8685  divmul13ap  8686  divmuleqap  8688  divdiv32ap  8691  divcanap7  8692  dmdcanap  8693  divdivap1  8694  divdivap2  8695  divadddivap  8698  divsubdivap  8699  conjmulap  8700  divneg2ap  8707  subrecap  8810  mvllmulapd  8813  lt2mul2div  8850  nndivtr  8975  2halves  9162  halfaddsub  9167  avgle1  9173  avgle2  9174  div4p1lem1div2  9186  un0addcl  9223  un0mulcl  9224  peano2z  9303  zneo  9368  nneoor  9369  nneo  9370  zeo  9372  zeo2  9373  deceq1  9402  qreccl  9656  xaddcom  9875  xnegdi  9882  xaddass  9883  xaddass2  9884  xpncan  9885  xleadd1a  9887  xltadd1  9890  xposdif  9896  xadd4d  9899  lincmb01cmp  10017  iccf1o  10018  fz0to4untppr  10138  fzosubel3  10210  qavgle  10273  2tnp1ge0ge0  10315  fldiv4p1lem1div2  10319  ceilqm1lt  10326  flqdiv  10335  modqlt  10347  modqdiffl  10349  modqcyc2  10374  modqaddabs  10376  mulqaddmodid  10378  mulp1mod1  10379  modqmuladd  10380  modqmuladdnn0  10382  qnegmod  10383  addmodid  10386  addmodidr  10387  modqadd2mod  10388  modqm1p1mod0  10389  modqmul12d  10392  modqnegd  10393  modqadd12d  10394  modqsub12d  10395  q2submod  10399  modqmulmodr  10404  modqaddmulmod  10405  modqsubdir  10407  modfzo0difsn  10409  modsumfzodifsn  10410  addmodlteq  10412  frecuzrdgsuc  10428  frecfzennn  10440  iseqovex  10470  seq3-1p  10494  seq3caopr2  10496  seq3caopr  10497  seq3id  10522  seq3homo  10524  seq3z  10525  expp1  10541  exprecap  10575  expaddzaplem  10577  expmulzap  10580  expdivap  10585  sqval  10592  sqsubswap  10594  sqdividap  10599  subsq  10641  subsq2  10642  binom2  10646  binom2sub  10648  mulbinom2  10651  binom3  10652  zesq  10653  bernneq2  10656  modqexp  10661  sqoddm1div8  10688  mulsubdivbinom2ap  10705  nn0opthlem1d  10714  nn0opthd  10716  nn0opth2d  10717  facp1  10724  facdiv  10732  facndiv  10733  faclbnd  10735  faclbnd2  10736  faclbnd3  10737  bcval  10743  bccmpl  10748  bcm1k  10754  bcp1n  10755  bcp1nk  10756  bcval5  10757  bcp1m1  10759  bcpasc  10760  bcn2m1  10763  hashprg  10802  hashdifpr  10814  hashfzo  10816  hashfzp1  10818  hashfz0  10819  hashxp  10820  zfz1isolemsplit  10832  zfz1isolem1  10834  seq3coll  10836  reval  10872  crre  10880  remim  10883  remul2  10896  immul2  10903  imval2  10917  cjdivap  10932  caucvgre  11004  cvg1nlemcau  11007  cvg1nlemres  11008  resqrexlemp1rp  11029  resqrexlemfp1  11032  resqrexlemover  11033  resqrexlemcalc1  11037  resqrexlemcalc3  11039  resqrexlemnm  11041  resqrexlemoverl  11044  resqrexlemglsq  11045  resqrexlemga  11046  resqrexlemsqa  11047  resqrexlemex  11048  resqrex  11049  sqrtdiv  11065  absvalsq  11076  absreimsq  11090  absdivap  11093  cau3lem  11137  maxabslemlub  11230  maxabslemval  11231  max0addsup  11242  minabs  11258  bdtrilem  11261  bdtri  11262  xrmaxaddlem  11282  xrmaxadd  11283  xrbdtri  11298  clim  11303  clim2  11305  climshftlemg  11324  climshft2  11328  climcn1  11330  climcn2  11331  subcn2  11333  reccn2ap  11335  climmulc2  11353  climsubc2  11355  clim2ser  11359  iser3shft  11368  climcau  11369  serf0  11374  fzosump1  11439  fsum1p  11440  fsump1  11442  sumsplitdc  11454  fsump1i  11455  mptfzshft  11464  fisum0diag2  11469  fsumconst  11476  fsumdifsnconst  11477  modfsummodlemstep  11479  modfsummod  11480  telfsumo  11488  fsumparts  11492  fsumrelem  11493  hash2iun1dif1  11502  binomlem  11505  binom  11506  binom1p  11507  binom1dif  11509  bcxmas  11511  isumsplit  11513  isum1p  11514  arisum  11520  arisum2  11521  trireciplem  11522  geoserap  11529  geolim  11533  geolim2  11534  georeclim  11535  geo2sum  11536  geoisum1  11541  cvgratnnlemseq  11548  cvgratnnlemsumlt  11550  cvgratnnlemfm  11551  cvgratz  11554  mertenslemi1  11557  mertenslem2  11558  mertensabs  11559  fprod1p  11621  fprodp1  11622  fprodcl2lem  11627  fprodfac  11637  fprodeq0  11639  fprodconst  11642  fprodrec  11651  fprodsplit1f  11656  fprodmodd  11663  efcllemp  11680  ef0lem  11682  efval  11683  esum  11684  ege2le3  11693  efaddlem  11696  efsep  11713  effsumlt  11714  eft0val  11715  efgt1p2  11717  efgt1p  11718  sinval  11724  cosval  11725  resinval  11737  recosval  11738  efi4p  11739  resin4p  11740  recos4p  11741  sinneg  11748  cosneg  11749  efival  11754  sinadd  11758  cosadd  11759  tanaddap  11761  sinmul  11766  cosmul  11767  cos2t  11772  cos2tsin  11773  ef01bndlem  11778  absefib  11792  demoivre  11794  demoivreALT  11795  eirraplem  11798  p1modz1  11815  dvdsmodexp  11816  moddvds  11820  mulmoddvds  11883  3dvds2dec  11885  zeo3  11887  odd2np1lem  11891  odd2np1  11892  oexpneg  11896  2tp1odd  11903  ltoddhalfle  11912  opoe  11914  opeo  11916  omeo  11917  m1expo  11919  m1exp1  11920  nn0o1gt2  11924  nn0o  11926  divalglemnn  11937  divalglemqt  11938  divalglemeunn  11940  divalglemex  11941  divalglemeuneg  11942  flodddiv4  11953  flodddiv4t2lthalf  11956  gcdaddm  11999  bezoutlemnewy  12011  bezoutlema  12014  bezoutlemb  12015  bezoutlemex  12016  bezoutlemaz  12018  mulgcd  12031  gcddiv  12034  gcdmultiplez  12036  rpmulgcd  12041  rplpwr  12042  uzwodc  12052  lcmgcdlem  12091  lcmgcd  12092  divgcdcoprmex  12116  cncongr2  12118  prmexpb  12165  rpexp  12167  rpexp1i  12168  sqrt2irrlem  12175  oddpwdclemxy  12183  oddpwdclemndvds  12185  sqpweven  12189  2sqpwodd  12190  sqne2sq  12191  qmuldeneqnum  12209  nn0gcdsq  12214  zgcdsq  12215  numdensq  12216  dfphi2  12234  phiprmpw  12236  phiprm  12237  eulerthlema  12244  eulerthlemh  12245  eulerthlemth  12246  fermltl  12248  prmdiv  12249  prmdiveq  12250  prmdivdiv  12251  hashgcdlem  12252  odzval  12255  odzcllem  12256  odzdvds  12259  vfermltl  12265  powm2modprm  12266  reumodprminv  12267  modprm0  12268  nnnn0modprm0  12269  modprmn0modprm0  12270  coprimeprodsq  12271  coprimeprodsq2  12272  pythagtriplem1  12279  pythagtriplem3  12281  pythagtriplem4  12282  pythagtriplem6  12284  pythagtriplem7  12285  pythagtriplem12  12289  pythagtriplem14  12291  pythagtriplem15  12292  pythagtriplem16  12293  pythagtriplem17  12294  pythagtriplem18  12295  pceu  12309  pczpre  12311  pcdiv  12316  pcqdiv  12321  pcrec  12322  pczndvds  12329  pcneg  12338  pc2dvds  12343  pcprmpw2  12346  pcaddlem  12352  pcadd  12353  fldivp1  12360  pockthlem  12368  pockthi  12370  4sqlem5  12394  4sqlem9  12398  4sqlem10  12399  4sqlem2  12401  4sqlem3  12402  4sqlem4  12404  mul4sqlem  12405  ennnfonelemkh  12427  ennnfonelemhf1o  12428  setscomd  12517  ressressg  12549  qusex  12764  qusin  12765  grpinvalem  12823  grpinva  12824  grprida  12825  isnsgrp  12831  sgrpass  12833  sgrp1  12836  sgrppropd  12838  mnd12g  12851  mndpropd  12863  mhmlin  12880  grprcan  12934  grpinvid1  12949  isgrpinv  12951  grplcan  12959  grpasscan1  12960  grplmulf1o  12971  grpinvadd  12975  grpinvsub  12979  grpsubsub4  12990  grppnpcan2  12991  grpnpncan  12992  dfgrp3mlem  12995  dfgrp3m  12996  grplactcnv  12999  imasgrp2  13005  mhmlem  13009  mhmid  13010  mhmmnd  13011  mulgnnp1  13023  mulg2  13024  mulgnn0p1  13026  mulgsubcl  13029  mulgneg  13033  mulgaddcomlem  13038  mulgaddcom  13039  mulgz  13043  mulgnn0dir  13045  mulgdirlem  13046  mulgdir  13047  mulgneg2  13049  mulgnnass  13050  mulgnn0ass  13051  mulgass  13052  mulgassr  13053  mulgmodid  13054  mulgsubdir  13055  isnsg3  13099  nmzsubg  13102  ssnmz  13103  0nsg  13106  eqger  13116  eqgid  13118  eqgcpbl  13120  ablsub2inv  13148  abladdsub4  13151  abladdsub  13152  ablpncan2  13153  ablpnpcan  13157  ablnncan  13158  ablnnncan1  13161  mgpress  13183  rngass  13191  rngdi  13192  rngdir  13193  rnglz  13197  rngmneg1  13199  rngsubdir  13204  rngpropd  13207  imasrng  13208  srgass  13223  srgmulgass  13241  srgpcomp  13242  srgpcompp  13243  srgpcomppsc  13244  ringpropd  13290  ringlz  13295  ring1eq0  13298  ringnegl  13301  ringmneg1  13303  ringsubdir  13307  mulgass2  13308  ring1  13309  imasring  13312  opprrng  13325  opprring  13327  unitgrp  13364  dvrcan1  13388  rdivmuldivd  13392  subrginv  13457  islmod  13480  lmodlema  13481  islmodd  13482  lmod0vs  13510  lmodvs0  13511  lmodvsmmulgdi  13512  lmodvneg1  13519  lmodvsneg  13520  lmodsubvs  13532  lmodsubdi  13533  lmodsubdir  13534  lmodprop2d  13537  rmodislmodlem  13539  rmodislmod  13540  lsssetm  13545  islssmd  13548  lssclg  13553  lssvacl  13554  lss1d  13572  lsspropdg  13620  sraval  13626  rnglidlmcl  13669  resttop  13966  restco  13970  restin  13972  lmfval  13988  cnprcl2k  14002  txrest  14072  txdis1cn  14074  cnmpt2res  14093  psmettri2  14124  psmettri  14126  xmettri2  14157  xmettri  14168  mettri  14169  metrtri  14173  blvalps  14184  blval  14185  xblss2  14201  blhalf  14204  comet  14295  xmetxp  14303  txmetcnp  14314  cnmet  14326  ioo2bl  14339  limcmpted  14428  limcimolemlt  14429  cnplimclemr  14434  limccnp2cntop  14442  reldvg  14444  dvfvalap  14446  dvidlemap  14456  dvconst  14457  dvcnp2cntop  14459  dvaddxxbr  14461  dvmulxxbr  14462  dvcoapbr  14467  dvcjbr  14468  dvexp  14471  dvrecap  14473  dvmptcmulcn  14479  dveflem  14483  sin0pilem1  14498  sinperlem  14525  ptolemy  14541  tangtx  14555  abssinper  14563  reexplog  14588  relogexp  14589  cxprec  14627  rpdivcxp  14628  cxpmul  14629  rpabscxpbnd  14655  rplogbval  14659  rplogbreexp  14667  rprelogbmul  14669  logbrec  14674  logbgcd1irraplemap  14683  binom4  14693  lgslem1  14697  lgslem4  14700  lgsval  14701  lgsfvalg  14702  lgsval2lem  14707  lgsval4lem  14708  lgsvalmod  14716  lgsneg  14721  lgsneg1  14722  lgsmod  14723  lgsdilem  14724  lgsdir2lem4  14728  lgsdir2  14730  lgsdirprm  14731  lgsdir  14732  lgsne0  14735  lgssq  14737  lgssq2  14738  lgsmulsqcoprm  14743  lgsdirnn0  14744  lgsdinn0  14745  lgseisenlem1  14746  lgseisenlem2  14747  m1lgs  14748  2lgsoddprmlem1  14749  2lgsoddprmlem2  14750  2lgsoddprmlem3  14755  2sqlem1  14757  2sqlem2  14758  mul2sq  14759  2sqlem3  14760  2sqlem4  14761  2sqlem8  14766  2sqlem9  14767  2sqlem10  14768  trilpolemeq1  15085  trilpolemlt1  15086  trirec0xor  15090  apdifflemf  15091  apdiff  15093