Theorem oveq1d 6100

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 6092	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A F C ) = ( B F C ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  fvoveq1d  6107  csbov2g  6127  caovassg  6248  caovdig  6264  caovdirg  6267  caov12d  6271  caov31d  6272  caov411d  6275  caofinvl  6328  suppofss1dcl  6504  suppofss2dcl  6505  omsuc  6745  nnmsucr  6761  nnm1  6798  nnm2  6799  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  isacnm  7559  addasspig  7697  mulasspig  7699  mulpipq2  7738  distrnqg  7754  ltsonq  7765  ltanqg  7767  ltmnqg  7768  ltexnqq  7775  archnqq  7784  prarloclemarch2  7786  enq0sym  7799  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  nqpnq0nq  7820  nq0m0r  7823  nq0a0  7824  nnanq0  7825  distrnq0  7826  addassnq0  7829  addpinq1  7831  prarloclemlo  7861  prarloclem3  7864  prarloclem5  7867  prarloclemcalc  7869  addnqprllem  7894  addnqprulem  7895  appdivnq  7930  recexprlem1ssl  8000  recexprlem1ssu  8001  ltmprr  8009  cauappcvgprlemladdru  8023  cauappcvgprlem1  8026  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemexb  8074  caucvgprprlem1  8076  addcmpblnr  8106  mulcmpblnrlemg  8107  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  ltsrprg  8114  1idsr  8135  pn0sr  8138  recexgt0sr  8140  mulgt0sr  8145  srpospr  8150  prsradd  8153  caucvgsrlemfv  8158  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffval  8163  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  caucvgsrlembnd  8168  caucvgsr  8169  map2psrprg  8172  pitonnlem1p1  8213  pitonnlem2  8214  pitonn  8215  recidpirqlemcalc  8224  ax1rid  8244  axrnegex  8246  axcnre  8248  recriota  8257  nntopi  8261  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  mul12  8456  mul4  8459  muladd11  8460  readdcan  8467  muladd11r  8483  add12  8485  cnegex  8505  addcan  8507  negeu  8518  pncan2  8534  addsubass  8537  addsub  8538  2addsub  8541  addsubeq4  8542  subid  8546  subid1  8547  npncan  8548  nppcan  8549  nnpcan  8550  nnncan1  8563  npncan3  8565  pnpcan  8566  pnncan  8568  ppncan  8569  addsub4  8570  negsub  8575  subneg  8576  subeqxfrd  8690  mvlraddd  8691  mvlladdd  8692  mvrraddd  8693  subaddeqd  8696  ine0  8722  mulneg1  8723  ltadd2  8748  apreap  8917  cru  8932  recexap  8983  mulcanapd  8991  div23ap  9023  div13ap  9025  divmulassap  9027  divmulasscomap  9028  divcanap4  9031  muldivdirap  9039  divsubdirap  9040  divmuldivap  9044  divdivdivap  9045  divcanap5  9046  divmul13ap  9047  divmuleqap  9049  divdiv32ap  9052  divcanap7  9053  dmdcanap  9054  divdivap1  9055  divdivap2  9056  divadddivap  9059  divsubdivap  9060  conjmulap  9061  divneg2ap  9068  subrecap  9171  mvllmulapd  9174  lt2mul2div  9211  nndivtr  9348  2halves  9538  halfaddsub  9543  subhalfhalf  9544  avgle1  9550  avgle2  9551  div4p1lem1div2  9563  un0addcl  9600  un0mulcl  9601  peano2z  9684  zneo  9751  nneoor  9752  nneo  9753  zeo  9755  zeo2  9756  deceq1  9785  qreccl  10051  xaddcom  10273  xnegdi  10280  xaddass  10281  xaddass2  10282  xpncan  10283  xleadd1a  10285  xltadd1  10288  xposdif  10294  xadd4d  10297  lincmb01cmp  10415  lincmble  10416  iccf1o  10417  fzspl  10486  fz0to4untppr  10541  fzo0addel  10616  fzosubel3  10624  qavgle  10703  2tnp1ge0ge0  10749  fldiv4p1lem1div2  10753  fldiv4lem1div2  10755  ceilqm1lt  10762  flqdiv  10771  modqlt  10783  modqdiffl  10785  modqcyc2  10810  modqaddabs  10812  mulqaddmodid  10814  mulp1mod1  10815  modqmuladd  10816  modqmuladdnn0  10818  qnegmod  10819  addmodid  10822  addmodidr  10823  modqadd2mod  10824  modqm1p1mod0  10825  modqmul12d  10828  modqnegd  10829  modqadd12d  10830  modqsub12d  10831  q2submod  10835  modqmulmodr  10840  modqaddmulmod  10841  modqsubdir  10843  modfzo0difsn  10845  modsumfzodifsn  10846  addmodlteq  10848  frecuzrdgsuc  10864  frecfzennn  10876  iseqovex  10908  seq3-1p  10940  seq3caopr2  10943  seqcaopr2g  10944  seq3caopr  10945  seqcaoprg  10946  seqf1oglem2a  10968  seqf1oglem1  10969  seqf1oglem2  10970  seq3id  10975  seq3homo  10977  seq3z  10978  seqhomog  10980  seqfeq4g  10981  expp1  10996  exprecap  11030  expaddzaplem  11032  expmulzap  11035  expdivap  11040  sqval  11047  sqsubswap  11049  sqdividap  11054  subsq  11096  subsq2  11097  binom2  11101  binom2sub  11103  mulbinom2  11106  binom3  11107  zesq  11109  bernneq2  11112  modqexp  11117  sqoddm1div8  11144  mulsubdivbinom2ap  11163  nn0opthlem1d  11172  nn0opthd  11174  nn0opth2d  11175  facp1  11182  facdiv  11190  facndiv  11191  faclbnd  11193  faclbnd2  11194  faclbnd3  11195  bcval  11201  bccmpl  11206  bcm1k  11212  bcp1n  11213  bcp1nk  11214  bcval5  11215  bcp1m1  11217  bcpasc  11218  bcm1n  11221  bcn2m1  11222  hashprg  11263  hashdifpr  11275  hashfzo  11277  hashfzp1  11279  hashfz0  11280  hashxp  11281  hashfibclem  11296  hashfibc  11297  hashf1  11301  zfz1isolemsplit  11304  zfz1isolem1  11306  seq3coll  11308  lswwrd  11365  ccatfvalfi  11374  ccatass  11390  lswccatn0lsw  11393  wrdlenccats1lenm1g  11418  ccatw2s1leng  11420  ccatswrd  11456  ccatpfx  11487  swrdpfx  11493  pfxpfx  11494  ccats1pfxeq  11500  wrdeqs1cat  11506  wrdind  11508  wrd2ind  11509  pfxccatpfx2  11523  pfxccatin12d  11531  cats1catd  11554  cats2catd  11555  s2leng  11575  s3s4d  11589  s2s5d  11590  s5s2d  11591  reval  11628  crre  11636  remim  11639  remul2  11652  immul2  11659  imval2  11673  sq01  11674  cjdivap  11689  caucvgre  11761  cvg1nlemcau  11764  cvg1nlemres  11765  resqrexlemp1rp  11786  resqrexlemfp1  11789  resqrexlemover  11790  resqrexlemcalc1  11794  resqrexlemcalc3  11796  resqrexlemnm  11798  resqrexlemoverl  11801  resqrexlemglsq  11802  resqrexlemga  11803  resqrexlemsqa  11804  resqrexlemex  11805  resqrex  11806  sqrtdiv  11822  absvalsq  11833  absreimsq  11847  absdivap  11850  cau3lem  11895  maxabslemlub  11988  maxabslemval  11989  max0addsup  12000  minabs  12017  bdtrilem  12021  bdtri  12022  xrmaxaddlem  12042  xrmaxadd  12043  xrbdtri  12058  clim  12063  clim2  12065  climshftlemg  12084  climshft2  12088  climcn1  12090  climcn2  12091  subcn2  12093  reccn2ap  12095  climmulc2  12113  climsubc2  12115  clim2ser  12119  iser3shft  12128  climcau  12129  serf0  12134  fzosump1  12200  fsum1p  12201  fsump1  12203  sumsplitdc  12215  fsump1i  12216  mptfzshft  12225  fisum0diag2  12230  fsumconst  12237  fsumdifsnconst  12238  modfsummodlemstep  12240  modfsummod  12241  telfsumo  12249  fsumparts  12253  fsumrelem  12254  hash2iun1dif1  12263  binomlem  12266  binom  12267  binom1p  12268  binom1dif  12270  bcxmas  12272  isumsplit  12274  isum1p  12275  arisum  12281  arisum2  12282  trireciplem  12283  geoserap  12290  geolim  12294  geolim2  12295  georeclim  12296  geo2sum  12297  geoisum1  12302  cvgratnnlemseq  12309  cvgratnnlemsumlt  12311  cvgratnnlemfm  12312  cvgratz  12315  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  fprod1p  12382  fprodp1  12383  fprodcl2lem  12388  fprodfac  12398  fprodeq0  12400  fprodconst  12403  fprodrec  12412  fprodsplit1f  12417  fprodmodd  12424  efcllemp  12441  ef0lem  12443  efval  12444  esum  12445  ege2le3  12454  efaddlem  12457  efsep  12474  effsumlt  12475  eft0val  12476  efgt1p2  12478  efgt1p  12479  sinval  12485  cosval  12486  resinval  12498  recosval  12499  efi4p  12500  resin4p  12501  recos4p  12502  sinneg  12509  cosneg  12510  efival  12515  sinadd  12519  cosadd  12520  tanaddap  12522  sinmul  12527  cosmul  12528  cos2t  12533  cos2tsin  12534  ef01bndlem  12539  absefib  12554  demoivre  12556  demoivreALT  12557  eirraplem  12560  p1modz1  12577  dvdsmodexp  12578  moddvds  12582  mulmoddvds  12646  3dvds2dec  12649  zeo3  12651  odd2np1lem  12655  odd2np1  12656  oexpneg  12660  2tp1odd  12667  ltoddhalfle  12676  opoe  12678  opeo  12680  omeo  12681  m1expo  12683  m1exp1  12684  nn0o1gt2  12688  nn0o  12690  divalglemnn  12701  divalglemqt  12702  divalglemeunn  12704  divalglemex  12705  divalglemeuneg  12706  flodddiv4  12719  flodddiv4t2lthalf  12722  bitsp1o  12736  bitsmod  12739  bitsinv1lem  12744  gcdaddm  12777  bezoutlemnewy  12789  bezoutlema  12792  bezoutlemb  12793  bezoutlemex  12794  bezoutlemaz  12796  mulgcd  12809  gcddiv  12812  gcdmultiplez  12814  rpmulgcd  12819  rplpwr  12820  uzwodc  12830  lcmgcdlem  12871  lcmgcd  12872  divgcdcoprmex  12896  cncongr2  12898  prmexpb  12946  rpexp  12948  rpexp1i  12949  sqrt2irrlem  12956  nnmaxpwlemxy  12964  nnmaxpwlemndvds  12966  sqpweven  12971  2sqpwodd  12972  sqne2sq  12973  qmuldeneqnum  12991  nn0gcdsq  12996  zgcdsq  12997  numdensq  12998  dfphi2  13018  phiprmpw  13020  phiprm  13021  eulerthlema  13028  eulerthlemh  13029  eulerthlemth  13030  fermltl  13032  prmdiv  13033  prmdiveq  13034  prmdivdiv  13035  hashgcdlem  13036  odzval  13040  odzcllem  13041  odzdvds  13044  vfermltl  13050  powm2modprm  13051  reumodprminv  13052  modprm0  13053  nnnn0modprm0  13054  modprmn0modprm0  13055  coprimeprodsq  13056  coprimeprodsq2  13057  pythagtriplem1  13064  pythagtriplem3  13066  pythagtriplem4  13067  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem12  13074  pythagtriplem14  13076  pythagtriplem15  13077  pythagtriplem16  13078  pythagtriplem17  13079  pythagtriplem18  13080  pceu  13094  pczpre  13096  pcdiv  13101  pcqdiv  13106  pcrec  13107  pczndvds  13115  pcneg  13124  pc2dvds  13129  pcprmpw2  13132  pcaddlem  13138  pcadd  13139  fldivp1  13147  pockthlem  13155  pockthi  13157  4sqlem5  13181  4sqlem9  13185  4sqlem10  13186  4sqlem2  13188  4sqlem3  13189  4sqlem4  13191  mul4sqlem  13192  4sqlem11  13200  4sqlem12  13201  4sqlem14  13203  4sqlem15  13204  4sqlem17  13206  4sqlem19  13208  ballotfilem2  13277  ballotfilemfp1  13280  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilem4  13290  ballotfilemi1  13294  ballotfilemii  13295  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemsval  13301  ballotfilemsdom  13304  ballotfilemsima  13308  ballotfilemieq  13309  ballotfilemfrci  13320  ballotfilemth  13330  ballotfi  13331  ennnfonelemkh  13352  ennnfonelemhf1o  13353  setscomd  13442  ressressg  13478  qusex  13695  qusin  13696  grpinvalem  13754  grpinva  13755  grprida  13756  gzsumsplit1r  13764  isnsgrp  13770  sgrpass  13772  sgrp1  13775  sgrppropd  13777  mnd12g  13790  mndpropd  13802  imasmnd2  13808  mhmex  13818  mhmlin  13823  grprcan  13891  grpinvid1  13906  isgrpinv  13908  grplcan  13916  grpasscan1  13917  grplmulf1o  13928  grpinvadd  13932  grpinvsub  13936  grpsubsub4  13947  grppnpcan2  13948  grpnpncan  13949  dfgrp3mlem  13952  dfgrp3m  13953  grplactcnv  13956  imasgrp2  13962  mhmlem  13966  mhmid  13967  mhmmnd  13968  mulgnnp1  13982  mulg2  13983  mulgnn0p1  13985  mulgsubcl  13988  mulgneg  13992  mulgaddcomlem  13997  mulgaddcom  13998  mulgz  14002  mulgnn0dir  14004  mulgdirlem  14005  mulgdir  14006  mulgneg2  14008  mulgnnass  14009  mulgnn0ass  14010  mulgass  14011  mulgassr  14012  mulgmodid  14013  mulgsubdir  14014  submmulg  14018  isnsg3  14059  nmzsubg  14062  ssnmz  14063  0nsg  14066  eqger  14076  eqgid  14078  eqgcpbl  14080  ghmlin  14100  ghmmulg  14108  ghmnsgima  14120  ghmnsgpreima  14121  conjghm  14128  conjnmz  14131  ablsub2inv  14164  abladdsub4  14167  abladdsub  14168  ablpncan2  14169  ablpnpcan  14173  ablnncan  14174  ablnnncan1  14177  gzsumconst  14192  gzsumsnfd  14196  gzsumsplit0  14197  gzsumshift  14198  gzsumgsum  14204  gsummptfidmadd  14210  gsumconstcmn  14215  prdssgrpd  14240  prdsidlem  14242  prdsmndd  14243  prdsinvlem  14245  mgpress  14279  rngass  14287  rngdi  14288  rngdir  14289  rnglz  14293  rngmneg1  14295  rngsubdir  14300  rngpropd  14303  imasrng  14304  srgass  14324  srgmulgass  14342  srgpcomp  14343  srgpcompp  14344  srgpcomppsc  14345  ringpropd  14392  ringlz  14397  ring1eq0  14402  ringnegl  14405  ringmneg1  14407  ringsubdir  14411  mulgass2  14412  ring1  14413  imasring  14418  opprrng  14431  opprring  14433  unitgrp  14472  dvrcan1  14496  rdivmuldivd  14500  subrginv  14594  resrhm  14605  unitrrg  14625  aprlring  14649  islmod  14676  lmodlema  14677  islmodd  14678  lmod0vs  14707  lmodvs0  14708  lmodvsmmulgdi  14709  lmodvneg1  14716  lmodvsneg  14717  lmodsubvs  14729  lmodsubdi  14730  lmodsubdir  14731  lmodprop2d  14734  rmodislmodlem  14736  rmodislmod  14737  lsssetm  14742  islssmd  14745  lssclg  14750  lssvacl  14751  lss1d  14769  lsspropdg  14817  sraval  14823  rnglidlmcl  14866  znunit  15043  isassa  15051  assalem  15052  assa2ass  15058  assapropd  15063  asclmul1  15078  assamulgscmlem2  15091  mplsubgfilemcl  15139  resttop  15320  restco  15324  restin  15326  lmfval  15343  cnprcl2k  15356  txrest  15426  txdis1cn  15428  cnmpt2res  15447  psmettri2  15478  psmettri  15480  xmettri2  15511  xmettri  15522  mettri  15523  metrtri  15527  blvalps  15538  blval  15539  xblss2  15555  blhalf  15558  comet  15649  xmetxp  15657  txmetcnp  15668  cnmet  15680  ioo2bl  15701  ivthreinc  15795  limcmpted  15813  limcimolemlt  15814  cnplimclemr  15819  limccnp2cntop  15827  reldvg  15829  dvfvalap  15831  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvconst  15844  dvconstre  15846  dvconstss  15848  dvcnp2cntop  15849  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  dvexp  15861  dvrecap  15863  dvmptcmulcn  15871  dveflem  15876  plyval  15882  elply2  15885  elplyr  15890  elplyd  15891  ply1termlem  15892  plyaddlem1  15897  plymullem1  15898  plycoeid3  15907  plycjlemc  15910  dvply1  15915  sin0pilem1  15932  sinperlem  15959  ptolemy  15975  tangtx  15989  abssinper  15997  reexplog  16023  relogexp  16024  cxprec  16065  rpdivcxp  16066  cxpmul  16067  rpabscxpbnd  16095  rplogbval  16100  rplogbreexp  16108  rprelogbmul  16110  logbrec  16115  logbgcd1irraplemap  16124  zprmlogbaplem1  16134  zprmlogbaplem3  16136  zprmlogbap  16137  binom4  16138  log2tlbndlog2  16139  log2ublem2  16141  birthdaylem2  16145  birthdaylem3  16146  pellexlem2  16149  pellexlem3  16150  wilthlem1  16151  ppiprm  16170  ppiqp1le  16173  mpodvdsmulf1o  16185  sgmppw  16187  0sgmppw  16188  1sgmprm  16189  1sgm2ppw  16190  ppiqub  16194  perfectlem1  16197  perfectlem2  16198  perfect  16199  bcctr  16200  pcbcctr  16201  bcmono  16202  bcp1ctr  16204  bclbnd  16205  bposlem3  16211  lgslem1  16217  lgslem4  16220  lgsval  16221  lgsfvalg  16222  lgsval2lem  16227  lgsval4lem  16228  lgsvalmod  16236  lgsneg  16241  lgsneg1  16242  lgsmod  16243  lgsdilem  16244  lgsdir2lem4  16248  lgsdir2  16250  lgsdirprm  16251  lgsdir  16252  lgsne0  16255  lgssq  16257  lgssq2  16258  lgsmulsqcoprm  16263  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem1a  16275  gausslemma2dlem4  16281  gausslemma2dlem5a  16282  gausslemma2dlem5  16283  gausslemma2dlem6  16284  gausslemma2dlem7  16285  gausslemma2d  16286  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem1  16298  lgsquad2lem2  16299  lgsquad3  16301  m1lgs  16302  2lgslem1a  16305  2lgslem1c  16307  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2lgslem3a1  16314  2lgslem3b1  16315  2lgslem3c1  16316  2lgslem3d1  16317  2lgsoddprmlem1  16322  2lgsoddprmlem2  16323  2lgsoddprmlem3  16328  2sqlem1  16331  2sqlem2  16332  mul2sq  16333  2sqlem3  16334  2sqlem4  16335  2sqlem8  16340  2sqlem9  16341  2sqlem10  16342  vdegp1bid  16654  uspgr2wlkeqi  16706  isclwwlk  16733  clwwlkccatlem  16739  clwwlknonex2  16778  repiecele0  17173  repiecege0  17174  repiecef  17175  trilpolemeq1  17187  trilpolemlt1  17188  trirec0xor  17192  apdifflemf  17193  apdiff  17195  qdiff  17196