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  8455  mul4  8458  muladd11  8459  readdcan  8466  muladd11r  8482  add12  8484  cnegex  8504  addcan  8506  negeu  8517  pncan2  8533  addsubass  8536  addsub  8537  2addsub  8540  addsubeq4  8541  subid  8545  subid1  8546  npncan  8547  nppcan  8548  nnpcan  8549  nnncan1  8562  npncan3  8564  pnpcan  8565  pnncan  8567  ppncan  8568  addsub4  8569  negsub  8574  subneg  8575  subeqxfrd  8689  mvlraddd  8690  mvlladdd  8691  mvrraddd  8692  subaddeqd  8695  ine0  8721  mulneg1  8722  ltadd2  8747  apreap  8915  cru  8930  recexap  8981  mulcanapd  8989  div23ap  9021  div13ap  9023  divmulassap  9025  divmulasscomap  9026  divcanap4  9029  muldivdirap  9037  divsubdirap  9038  divmuldivap  9042  divdivdivap  9043  divcanap5  9044  divmul13ap  9045  divmuleqap  9047  divdiv32ap  9050  divcanap7  9051  dmdcanap  9052  divdivap1  9053  divdivap2  9054  divadddivap  9057  divsubdivap  9058  conjmulap  9059  divneg2ap  9066  subrecap  9169  mvllmulapd  9172  lt2mul2div  9209  nndivtr  9346  2halves  9534  halfaddsub  9539  subhalfhalf  9540  avgle1  9546  avgle2  9547  div4p1lem1div2  9559  un0addcl  9596  un0mulcl  9597  peano2z  9680  zneo  9747  nneoor  9748  nneo  9749  zeo  9751  zeo2  9752  deceq1  9781  qreccl  10042  xaddcom  10263  xnegdi  10270  xaddass  10271  xaddass2  10272  xpncan  10273  xleadd1a  10275  xltadd1  10278  xposdif  10284  xadd4d  10287  lincmb01cmp  10405  lincmble  10406  iccf1o  10407  fzspl  10476  fz0to4untppr  10531  fzo0addel  10606  fzosubel3  10614  qavgle  10693  2tnp1ge0ge0  10736  fldiv4p1lem1div2  10740  fldiv4lem1div2  10742  ceilqm1lt  10749  flqdiv  10758  modqlt  10770  modqdiffl  10772  modqcyc2  10797  modqaddabs  10799  mulqaddmodid  10801  mulp1mod1  10802  modqmuladd  10803  modqmuladdnn0  10805  qnegmod  10806  addmodid  10809  addmodidr  10810  modqadd2mod  10811  modqm1p1mod0  10812  modqmul12d  10815  modqnegd  10816  modqadd12d  10817  modqsub12d  10818  q2submod  10822  modqmulmodr  10827  modqaddmulmod  10828  modqsubdir  10830  modfzo0difsn  10832  modsumfzodifsn  10833  addmodlteq  10835  frecuzrdgsuc  10851  frecfzennn  10863  iseqovex  10895  seq3-1p  10927  seq3caopr2  10930  seqcaopr2g  10931  seq3caopr  10932  seqcaoprg  10933  seqf1oglem2a  10955  seqf1oglem1  10956  seqf1oglem2  10957  seq3id  10962  seq3homo  10964  seq3z  10965  seqhomog  10967  seqfeq4g  10968  expp1  10983  exprecap  11017  expaddzaplem  11019  expmulzap  11022  expdivap  11027  sqval  11034  sqsubswap  11036  sqdividap  11041  subsq  11083  subsq2  11084  binom2  11088  binom2sub  11090  mulbinom2  11093  binom3  11094  zesq  11096  bernneq2  11099  modqexp  11104  sqoddm1div8  11131  mulsubdivbinom2ap  11149  nn0opthlem1d  11158  nn0opthd  11160  nn0opth2d  11161  facp1  11168  facdiv  11176  facndiv  11177  faclbnd  11179  faclbnd2  11180  faclbnd3  11181  bcval  11187  bccmpl  11192  bcm1k  11198  bcp1n  11199  bcp1nk  11200  bcval5  11201  bcp1m1  11203  bcpasc  11204  bcm1n  11207  bcn2m1  11208  hashprg  11249  hashdifpr  11261  hashfzo  11263  hashfzp1  11265  hashfz0  11266  hashxp  11267  hashfibclem  11282  hashfibc  11283  hashf1  11287  zfz1isolemsplit  11290  zfz1isolem1  11292  seq3coll  11294  lswwrd  11351  ccatfvalfi  11360  ccatass  11376  lswccatn0lsw  11379  wrdlenccats1lenm1g  11404  ccatw2s1leng  11406  ccatswrd  11442  ccatpfx  11473  swrdpfx  11479  pfxpfx  11480  ccats1pfxeq  11486  wrdeqs1cat  11492  wrdind  11494  wrd2ind  11495  pfxccatpfx2  11509  pfxccatin12d  11517  cats1catd  11540  cats2catd  11541  s2leng  11561  s3s4d  11575  s2s5d  11576  s5s2d  11577  reval  11614  crre  11622  remim  11625  remul2  11638  immul2  11645  imval2  11659  sq01  11660  cjdivap  11675  caucvgre  11747  cvg1nlemcau  11750  cvg1nlemres  11751  resqrexlemp1rp  11772  resqrexlemfp1  11775  resqrexlemover  11776  resqrexlemcalc1  11780  resqrexlemcalc3  11782  resqrexlemnm  11784  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemga  11789  resqrexlemsqa  11790  resqrexlemex  11791  resqrex  11792  sqrtdiv  11808  absvalsq  11819  absreimsq  11833  absdivap  11836  cau3lem  11880  maxabslemlub  11973  maxabslemval  11974  max0addsup  11985  minabs  12002  bdtrilem  12005  bdtri  12006  xrmaxaddlem  12026  xrmaxadd  12027  xrbdtri  12042  clim  12047  clim2  12049  climshftlemg  12068  climshft2  12072  climcn1  12074  climcn2  12075  subcn2  12077  reccn2ap  12079  climmulc2  12097  climsubc2  12099  clim2ser  12103  iser3shft  12112  climcau  12113  serf0  12118  fzosump1  12184  fsum1p  12185  fsump1  12187  sumsplitdc  12199  fsump1i  12200  mptfzshft  12209  fisum0diag2  12214  fsumconst  12221  fsumdifsnconst  12222  modfsummodlemstep  12224  modfsummod  12225  telfsumo  12233  fsumparts  12237  fsumrelem  12238  hash2iun1dif1  12247  binomlem  12250  binom  12251  binom1p  12252  binom1dif  12254  bcxmas  12256  isumsplit  12258  isum1p  12259  arisum  12265  arisum2  12266  trireciplem  12267  geoserap  12274  geolim  12278  geolim2  12279  georeclim  12280  geo2sum  12281  geoisum1  12286  cvgratnnlemseq  12293  cvgratnnlemsumlt  12295  cvgratnnlemfm  12296  cvgratz  12299  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  fprod1p  12366  fprodp1  12367  fprodcl2lem  12372  fprodfac  12382  fprodeq0  12384  fprodconst  12387  fprodrec  12396  fprodsplit1f  12401  fprodmodd  12408  efcllemp  12425  ef0lem  12427  efval  12428  esum  12429  ege2le3  12438  efaddlem  12441  efsep  12458  effsumlt  12459  eft0val  12460  efgt1p2  12462  efgt1p  12463  sinval  12469  cosval  12470  resinval  12482  recosval  12483  efi4p  12484  resin4p  12485  recos4p  12486  sinneg  12493  cosneg  12494  efival  12499  sinadd  12503  cosadd  12504  tanaddap  12506  sinmul  12511  cosmul  12512  cos2t  12517  cos2tsin  12518  ef01bndlem  12523  absefib  12538  demoivre  12540  demoivreALT  12541  eirraplem  12544  p1modz1  12561  dvdsmodexp  12562  moddvds  12566  mulmoddvds  12630  3dvds2dec  12633  zeo3  12635  odd2np1lem  12639  odd2np1  12640  oexpneg  12644  2tp1odd  12651  ltoddhalfle  12660  opoe  12662  opeo  12664  omeo  12665  m1expo  12667  m1exp1  12668  nn0o1gt2  12672  nn0o  12674  divalglemnn  12685  divalglemqt  12686  divalglemeunn  12688  divalglemex  12689  divalglemeuneg  12690  flodddiv4  12703  flodddiv4t2lthalf  12706  bitsp1o  12720  bitsmod  12723  bitsinv1lem  12728  gcdaddm  12761  bezoutlemnewy  12773  bezoutlema  12776  bezoutlemb  12777  bezoutlemex  12778  bezoutlemaz  12780  mulgcd  12793  gcddiv  12796  gcdmultiplez  12798  rpmulgcd  12803  rplpwr  12804  uzwodc  12814  lcmgcdlem  12855  lcmgcd  12856  divgcdcoprmex  12880  cncongr2  12882  prmexpb  12929  rpexp  12931  rpexp1i  12932  sqrt2irrlem  12939  oddpwdclemxy  12947  oddpwdclemndvds  12949  sqpweven  12953  2sqpwodd  12954  sqne2sq  12955  qmuldeneqnum  12973  nn0gcdsq  12978  zgcdsq  12979  numdensq  12980  dfphi2  12998  phiprmpw  13000  phiprm  13001  eulerthlema  13008  eulerthlemh  13009  eulerthlemth  13010  fermltl  13012  prmdiv  13013  prmdiveq  13014  prmdivdiv  13015  hashgcdlem  13016  odzval  13020  odzcllem  13021  odzdvds  13024  vfermltl  13030  powm2modprm  13031  reumodprminv  13032  modprm0  13033  nnnn0modprm0  13034  modprmn0modprm0  13035  coprimeprodsq  13036  coprimeprodsq2  13037  pythagtriplem1  13044  pythagtriplem3  13046  pythagtriplem4  13047  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem15  13057  pythagtriplem16  13058  pythagtriplem17  13059  pythagtriplem18  13060  pceu  13074  pczpre  13076  pcdiv  13081  pcqdiv  13086  pcrec  13087  pczndvds  13095  pcneg  13104  pc2dvds  13109  pcprmpw2  13112  pcaddlem  13118  pcadd  13119  fldivp1  13127  pockthlem  13135  pockthi  13137  4sqlem5  13161  4sqlem9  13165  4sqlem10  13166  4sqlem2  13168  4sqlem3  13169  4sqlem4  13171  mul4sqlem  13172  4sqlem11  13180  4sqlem12  13181  4sqlem14  13183  4sqlem15  13184  4sqlem17  13186  4sqlem19  13188  ballotfilem2  13228  ballotfilemfp1  13231  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilem4  13241  ballotfilemi1  13245  ballotfilemii  13246  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemsval  13252  ballotfilemsdom  13255  ballotfilemsima  13259  ballotfilemieq  13260  ballotfilemfrci  13271  ballotfilemth  13281  ballotfi  13282  ennnfonelemkh  13303  ennnfonelemhf1o  13304  setscomd  13393  ressressg  13429  qusex  13646  qusin  13647  grpinvalem  13705  grpinva  13706  grprida  13707  gzsumsplit1r  13715  isnsgrp  13721  sgrpass  13723  sgrp1  13726  sgrppropd  13728  mnd12g  13741  mndpropd  13753  imasmnd2  13759  mhmex  13769  mhmlin  13774  grprcan  13842  grpinvid1  13857  isgrpinv  13859  grplcan  13867  grpasscan1  13868  grplmulf1o  13879  grpinvadd  13883  grpinvsub  13887  grpsubsub4  13898  grppnpcan2  13899  grpnpncan  13900  dfgrp3mlem  13903  dfgrp3m  13904  grplactcnv  13907  imasgrp2  13913  mhmlem  13917  mhmid  13918  mhmmnd  13919  mulgnnp1  13933  mulg2  13934  mulgnn0p1  13936  mulgsubcl  13939  mulgneg  13943  mulgaddcomlem  13948  mulgaddcom  13949  mulgz  13953  mulgnn0dir  13955  mulgdirlem  13956  mulgdir  13957  mulgneg2  13959  mulgnnass  13960  mulgnn0ass  13961  mulgass  13962  mulgassr  13963  mulgmodid  13964  mulgsubdir  13965  submmulg  13969  isnsg3  14010  nmzsubg  14013  ssnmz  14014  0nsg  14017  eqger  14027  eqgid  14029  eqgcpbl  14031  ghmlin  14051  ghmmulg  14059  ghmnsgima  14071  ghmnsgpreima  14072  conjghm  14079  conjnmz  14082  ablsub2inv  14115  abladdsub4  14118  abladdsub  14119  ablpncan2  14120  ablpnpcan  14124  ablnncan  14125  ablnnncan1  14128  gzsumconst  14143  gzsumsnfd  14147  gzsumsplit0  14148  gzsumshift  14149  gzsumgsum  14155  gsummptfidmadd  14161  gsumconstcmn  14166  prdssgrpd  14191  prdsidlem  14193  prdsmndd  14194  prdsinvlem  14196  mgpress  14230  rngass  14238  rngdi  14239  rngdir  14240  rnglz  14244  rngmneg1  14246  rngsubdir  14251  rngpropd  14254  imasrng  14255  srgass  14275  srgmulgass  14293  srgpcomp  14294  srgpcompp  14295  srgpcomppsc  14296  ringpropd  14343  ringlz  14348  ring1eq0  14353  ringnegl  14356  ringmneg1  14358  ringsubdir  14362  mulgass2  14363  ring1  14364  imasring  14369  opprrng  14382  opprring  14384  unitgrp  14423  dvrcan1  14447  rdivmuldivd  14451  subrginv  14545  resrhm  14556  unitrrg  14576  aprlring  14600  islmod  14627  lmodlema  14628  islmodd  14629  lmod0vs  14658  lmodvs0  14659  lmodvsmmulgdi  14660  lmodvneg1  14667  lmodvsneg  14668  lmodsubvs  14680  lmodsubdi  14681  lmodsubdir  14682  lmodprop2d  14685  rmodislmodlem  14687  rmodislmod  14688  lsssetm  14693  islssmd  14696  lssclg  14701  lssvacl  14702  lss1d  14720  lsspropdg  14768  sraval  14774  rnglidlmcl  14817  znunit  14994  isassa  15002  assalem  15003  assa2ass  15009  assapropd  15014  asclmul1  15029  assamulgscmlem2  15042  mplsubgfilemcl  15090  resttop  15271  restco  15275  restin  15277  lmfval  15294  cnprcl2k  15307  txrest  15377  txdis1cn  15379  cnmpt2res  15398  psmettri2  15429  psmettri  15431  xmettri2  15462  xmettri  15473  mettri  15474  metrtri  15478  blvalps  15489  blval  15490  xblss2  15506  blhalf  15509  comet  15600  xmetxp  15608  txmetcnp  15619  cnmet  15631  ioo2bl  15652  ivthreinc  15746  limcmpted  15764  limcimolemlt  15765  cnplimclemr  15770  limccnp2cntop  15778  reldvg  15780  dvfvalap  15782  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvconst  15795  dvconstre  15797  dvconstss  15799  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvcjbr  15809  dvexp  15812  dvrecap  15814  dvmptcmulcn  15822  dveflem  15827  plyval  15833  elply2  15836  elplyr  15841  elplyd  15842  ply1termlem  15843  plyaddlem1  15848  plymullem1  15849  plycoeid3  15858  plycjlemc  15861  dvply1  15866  sin0pilem1  15882  sinperlem  15909  ptolemy  15925  tangtx  15939  abssinper  15947  reexplog  15972  relogexp  15973  cxprec  16012  rpdivcxp  16013  cxpmul  16014  rpabscxpbnd  16042  rplogbval  16047  rplogbreexp  16055  rprelogbmul  16057  logbrec  16062  logbgcd1irraplemap  16071  binom4  16081  log2tlbndlog2  16082  log2ublem2  16084  birthdaylem2  16088  birthdaylem3  16089  pellexlem2  16092  pellexlem3  16093  wilthlem1  16094  mpodvdsmulf1o  16104  sgmppw  16106  0sgmppw  16107  1sgmprm  16108  1sgm2ppw  16109  perfectlem1  16113  perfectlem2  16114  perfect  16115  lgslem1  16119  lgslem4  16122  lgsval  16123  lgsfvalg  16124  lgsval2lem  16129  lgsval4lem  16130  lgsvalmod  16138  lgsneg  16143  lgsneg1  16144  lgsmod  16145  lgsdilem  16146  lgsdir2lem4  16150  lgsdir2  16152  lgsdirprm  16153  lgsdir  16154  lgsne0  16157  lgssq  16159  lgssq2  16160  lgsmulsqcoprm  16165  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem1a  16177  gausslemma2dlem4  16183  gausslemma2dlem5a  16184  gausslemma2dlem5  16185  gausslemma2dlem6  16186  gausslemma2dlem7  16187  gausslemma2d  16188  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgseisen  16193  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem1  16200  lgsquad2lem2  16201  lgsquad3  16203  m1lgs  16204  2lgslem1a  16207  2lgslem1c  16209  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgslem3a1  16216  2lgslem3b1  16217  2lgslem3c1  16218  2lgslem3d1  16219  2lgsoddprmlem1  16224  2lgsoddprmlem2  16225  2lgsoddprmlem3  16230  2sqlem1  16233  2sqlem2  16234  mul2sq  16235  2sqlem3  16236  2sqlem4  16237  2sqlem8  16242  2sqlem9  16243  2sqlem10  16244  vdegp1bid  16556  uspgr2wlkeqi  16608  isclwwlk  16635  clwwlkccatlem  16641  clwwlknonex2  16680  repiecele0  17075  repiecege0  17076  repiecef  17077  trilpolemeq1  17089  trilpolemlt1  17090  trirec0xor  17094  apdifflemf  17095  apdiff  17097  qdiff  17098