Theorem oveq1d 6093

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 6085	. 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 1402  (class class class)co 6078

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 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 theorem 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 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6081

This theorem is referenced by:  fvoveq1d  6100  csbov2g  6120  caovassg  6241  caovdig  6257  caovdirg  6260  caov12d  6264  caov31d  6265  caov411d  6268  caofinvl  6321  suppofss1dcl  6497  suppofss2dcl  6498  omsuc  6738  nnmsucr  6754  nnm1  6791  nnm2  6792  ecovass  6911  ecoviass  6912  ecovdi  6913  ecovidi  6914  isacnm  7552  addasspig  7690  mulasspig  7692  mulpipq2  7731  distrnqg  7747  ltsonq  7758  ltanqg  7760  ltmnqg  7761  ltexnqq  7768  archnqq  7777  prarloclemarch2  7779  enq0sym  7792  addnq0mo  7807  mulnq0mo  7808  addnnnq0  7809  nqpnq0nq  7813  nq0m0r  7816  nq0a0  7817  nnanq0  7818  distrnq0  7819  addassnq0  7822  addpinq1  7824  prarloclemlo  7854  prarloclem3  7857  prarloclem5  7860  prarloclemcalc  7862  addnqprllem  7887  addnqprulem  7888  appdivnq  7923  recexprlem1ssl  7993  recexprlem1ssu  7994  ltmprr  8002  cauappcvgprlemladdru  8016  cauappcvgprlem1  8019  caucvgprlemnkj  8026  caucvgprlemnbj  8027  caucvgprlemcl  8036  caucvgprlemladdfu  8037  caucvgprlemladdrl  8038  caucvgprlem1  8039  caucvgprprlemcbv  8047  caucvgprprlemval  8048  caucvgprprlemexb  8067  caucvgprprlem1  8069  addcmpblnr  8099  mulcmpblnrlemg  8100  addsrmo  8103  mulsrmo  8104  addsrpr  8105  mulsrpr  8106  ltsrprg  8107  1idsr  8128  pn0sr  8131  recexgt0sr  8133  mulgt0sr  8138  srpospr  8143  prsradd  8146  caucvgsrlemfv  8151  caucvgsrlemcau  8153  caucvgsrlemgt1  8155  caucvgsrlemoffval  8156  caucvgsrlemoffcau  8158  caucvgsrlemoffres  8160  caucvgsrlembnd  8161  caucvgsr  8162  map2psrprg  8165  pitonnlem1p1  8206  pitonnlem2  8207  pitonn  8208  recidpirqlemcalc  8217  ax1rid  8237  axrnegex  8239  axcnre  8241  recriota  8250  nntopi  8254  axcaucvglemval  8257  axcaucvglemcau  8258  axcaucvglemres  8259  mul12  8448  mul4  8451  muladd11  8452  readdcan  8459  muladd11r  8475  add12  8477  cnegex  8497  addcan  8499  negeu  8510  pncan2  8526  addsubass  8529  addsub  8530  2addsub  8533  addsubeq4  8534  subid  8538  subid1  8539  npncan  8540  nppcan  8541  nnpcan  8542  nnncan1  8555  npncan3  8557  pnpcan  8558  pnncan  8560  ppncan  8561  addsub4  8562  negsub  8567  subneg  8568  subeqxfrd  8682  mvlraddd  8683  mvlladdd  8684  mvrraddd  8685  subaddeqd  8688  ine0  8714  mulneg1  8715  ltadd2  8740  apreap  8908  cru  8923  recexap  8974  mulcanapd  8982  div23ap  9014  div13ap  9016  divmulassap  9018  divmulasscomap  9019  divcanap4  9022  muldivdirap  9030  divsubdirap  9031  divmuldivap  9035  divdivdivap  9036  divcanap5  9037  divmul13ap  9038  divmuleqap  9040  divdiv32ap  9043  divcanap7  9044  dmdcanap  9045  divdivap1  9046  divdivap2  9047  divadddivap  9050  divsubdivap  9051  conjmulap  9052  divneg2ap  9059  subrecap  9162  mvllmulapd  9165  lt2mul2div  9202  nndivtr  9328  2halves  9516  halfaddsub  9521  subhalfhalf  9522  avgle1  9528  avgle2  9529  div4p1lem1div2  9541  un0addcl  9578  un0mulcl  9579  peano2z  9662  zneo  9729  nneoor  9730  nneo  9731  zeo  9733  zeo2  9734  deceq1  9763  qreccl  10024  xaddcom  10245  xnegdi  10252  xaddass  10253  xaddass2  10254  xpncan  10255  xleadd1a  10257  xltadd1  10260  xposdif  10266  xadd4d  10269  lincmb01cmp  10387  lincmble  10388  iccf1o  10389  fzspl  10457  fz0to4untppr  10512  fzo0addel  10587  fzosubel3  10595  qavgle  10674  2tnp1ge0ge0  10717  fldiv4p1lem1div2  10721  fldiv4lem1div2  10723  ceilqm1lt  10730  flqdiv  10739  modqlt  10751  modqdiffl  10753  modqcyc2  10778  modqaddabs  10780  mulqaddmodid  10782  mulp1mod1  10783  modqmuladd  10784  modqmuladdnn0  10786  qnegmod  10787  addmodid  10790  addmodidr  10791  modqadd2mod  10792  modqm1p1mod0  10793  modqmul12d  10796  modqnegd  10797  modqadd12d  10798  modqsub12d  10799  q2submod  10803  modqmulmodr  10808  modqaddmulmod  10809  modqsubdir  10811  modfzo0difsn  10813  modsumfzodifsn  10814  addmodlteq  10816  frecuzrdgsuc  10832  frecfzennn  10844  iseqovex  10876  seq3-1p  10908  seq3caopr2  10911  seqcaopr2g  10912  seq3caopr  10913  seqcaoprg  10914  seqf1oglem2a  10936  seqf1oglem1  10937  seqf1oglem2  10938  seq3id  10943  seq3homo  10945  seq3z  10946  seqhomog  10948  seqfeq4g  10949  expp1  10964  exprecap  10998  expaddzaplem  11000  expmulzap  11003  expdivap  11008  sqval  11015  sqsubswap  11017  sqdividap  11022  subsq  11064  subsq2  11065  binom2  11069  binom2sub  11071  mulbinom2  11074  binom3  11075  zesq  11077  bernneq2  11080  modqexp  11085  sqoddm1div8  11112  mulsubdivbinom2ap  11130  nn0opthlem1d  11139  nn0opthd  11141  nn0opth2d  11142  facp1  11149  facdiv  11157  facndiv  11158  faclbnd  11160  faclbnd2  11161  faclbnd3  11162  bcval  11168  bccmpl  11173  bcm1k  11179  bcp1n  11180  bcp1nk  11181  bcval5  11182  bcp1m1  11184  bcpasc  11185  bcm1n  11188  bcn2m1  11189  hashprg  11230  hashdifpr  11242  hashfzo  11244  hashfzp1  11246  hashfz0  11247  hashxp  11248  hashfibclem  11263  hashfibc  11264  hashf1  11268  zfz1isolemsplit  11271  zfz1isolem1  11273  seq3coll  11275  lswwrd  11332  ccatfvalfi  11341  ccatass  11357  lswccatn0lsw  11360  wrdlenccats1lenm1g  11385  ccatw2s1leng  11387  ccatswrd  11423  ccatpfx  11454  swrdpfx  11460  pfxpfx  11461  ccats1pfxeq  11467  wrdeqs1cat  11473  wrdind  11475  wrd2ind  11476  pfxccatpfx2  11490  pfxccatin12d  11498  cats1catd  11521  cats2catd  11522  s2leng  11542  s3s4d  11556  s2s5d  11557  s5s2d  11558  reval  11595  crre  11603  remim  11606  remul2  11619  immul2  11626  imval2  11640  sq01  11641  cjdivap  11656  caucvgre  11728  cvg1nlemcau  11731  cvg1nlemres  11732  resqrexlemp1rp  11753  resqrexlemfp1  11756  resqrexlemover  11757  resqrexlemcalc1  11761  resqrexlemcalc3  11763  resqrexlemnm  11765  resqrexlemoverl  11768  resqrexlemglsq  11769  resqrexlemga  11770  resqrexlemsqa  11771  resqrexlemex  11772  resqrex  11773  sqrtdiv  11789  absvalsq  11800  absreimsq  11814  absdivap  11817  cau3lem  11861  maxabslemlub  11954  maxabslemval  11955  max0addsup  11966  minabs  11983  bdtrilem  11986  bdtri  11987  xrmaxaddlem  12007  xrmaxadd  12008  xrbdtri  12023  clim  12028  clim2  12030  climshftlemg  12049  climshft2  12053  climcn1  12055  climcn2  12056  subcn2  12058  reccn2ap  12060  climmulc2  12078  climsubc2  12080  clim2ser  12084  iser3shft  12093  climcau  12094  serf0  12099  fzosump1  12165  fsum1p  12166  fsump1  12168  sumsplitdc  12180  fsump1i  12181  mptfzshft  12190  fisum0diag2  12195  fsumconst  12202  fsumdifsnconst  12203  modfsummodlemstep  12205  modfsummod  12206  telfsumo  12214  fsumparts  12218  fsumrelem  12219  hash2iun1dif1  12228  binomlem  12231  binom  12232  binom1p  12233  binom1dif  12235  bcxmas  12237  isumsplit  12239  isum1p  12240  arisum  12246  arisum2  12247  trireciplem  12248  geoserap  12255  geolim  12259  geolim2  12260  georeclim  12261  geo2sum  12262  geoisum1  12267  cvgratnnlemseq  12274  cvgratnnlemsumlt  12276  cvgratnnlemfm  12277  cvgratz  12280  mertenslemi1  12283  mertenslem2  12284  mertensabs  12285  fprod1p  12347  fprodp1  12348  fprodcl2lem  12353  fprodfac  12363  fprodeq0  12365  fprodconst  12368  fprodrec  12377  fprodsplit1f  12382  fprodmodd  12389  efcllemp  12406  ef0lem  12408  efval  12409  esum  12410  ege2le3  12419  efaddlem  12422  efsep  12439  effsumlt  12440  eft0val  12441  efgt1p2  12443  efgt1p  12444  sinval  12450  cosval  12451  resinval  12463  recosval  12464  efi4p  12465  resin4p  12466  recos4p  12467  sinneg  12474  cosneg  12475  efival  12480  sinadd  12484  cosadd  12485  tanaddap  12487  sinmul  12492  cosmul  12493  cos2t  12498  cos2tsin  12499  ef01bndlem  12504  absefib  12519  demoivre  12521  demoivreALT  12522  eirraplem  12525  p1modz1  12542  dvdsmodexp  12543  moddvds  12547  mulmoddvds  12611  3dvds2dec  12614  zeo3  12616  odd2np1lem  12620  odd2np1  12621  oexpneg  12625  2tp1odd  12632  ltoddhalfle  12641  opoe  12643  opeo  12645  omeo  12646  m1expo  12648  m1exp1  12649  nn0o1gt2  12653  nn0o  12655  divalglemnn  12666  divalglemqt  12667  divalglemeunn  12669  divalglemex  12670  divalglemeuneg  12671  flodddiv4  12684  flodddiv4t2lthalf  12687  bitsp1o  12701  bitsmod  12704  bitsinv1lem  12709  gcdaddm  12742  bezoutlemnewy  12754  bezoutlema  12757  bezoutlemb  12758  bezoutlemex  12759  bezoutlemaz  12761  mulgcd  12774  gcddiv  12777  gcdmultiplez  12779  rpmulgcd  12784  rplpwr  12785  uzwodc  12795  lcmgcdlem  12836  lcmgcd  12837  divgcdcoprmex  12861  cncongr2  12863  prmexpb  12910  rpexp  12912  rpexp1i  12913  sqrt2irrlem  12920  oddpwdclemxy  12928  oddpwdclemndvds  12930  sqpweven  12934  2sqpwodd  12935  sqne2sq  12936  qmuldeneqnum  12954  nn0gcdsq  12959  zgcdsq  12960  numdensq  12961  dfphi2  12979  phiprmpw  12981  phiprm  12982  eulerthlema  12989  eulerthlemh  12990  eulerthlemth  12991  fermltl  12993  prmdiv  12994  prmdiveq  12995  prmdivdiv  12996  hashgcdlem  12997  odzval  13001  odzcllem  13002  odzdvds  13005  vfermltl  13011  powm2modprm  13012  reumodprminv  13013  modprm0  13014  nnnn0modprm0  13015  modprmn0modprm0  13016  coprimeprodsq  13017  coprimeprodsq2  13018  pythagtriplem1  13025  pythagtriplem3  13027  pythagtriplem4  13028  pythagtriplem6  13030  pythagtriplem7  13031  pythagtriplem12  13035  pythagtriplem14  13037  pythagtriplem15  13038  pythagtriplem16  13039  pythagtriplem17  13040  pythagtriplem18  13041  pceu  13055  pczpre  13057  pcdiv  13062  pcqdiv  13067  pcrec  13068  pczndvds  13076  pcneg  13085  pc2dvds  13090  pcprmpw2  13093  pcaddlem  13099  pcadd  13100  fldivp1  13108  pockthlem  13116  pockthi  13118  4sqlem5  13142  4sqlem9  13146  4sqlem10  13147  4sqlem2  13149  4sqlem3  13150  4sqlem4  13152  mul4sqlem  13153  4sqlem11  13161  4sqlem12  13162  4sqlem14  13164  4sqlem15  13165  4sqlem17  13167  4sqlem19  13169  ballotfilem2  13209  ballotfilemfp1  13212  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfilem4  13222  ballotfilemi1  13226  ballotfilemii  13227  ballotfilemic  13231  ballotfilem1c  13232  ballotfilemsval  13233  ballotfilemsdom  13236  ballotfilemsima  13240  ballotfilemieq  13241  ballotfilemfrci  13252  ballotfilemth  13262  ballotfi  13263  ennnfonelemkh  13284  ennnfonelemhf1o  13285  setscomd  13374  ressressg  13409  qusex  13626  qusin  13627  grpinvalem  13685  grpinva  13686  grprida  13687  gzsumsplit1r  13695  isnsgrp  13701  sgrpass  13703  sgrp1  13706  sgrppropd  13708  mnd12g  13721  mndpropd  13733  imasmnd2  13739  mhmex  13749  mhmlin  13754  grprcan  13822  grpinvid1  13837  isgrpinv  13839  grplcan  13847  grpasscan1  13848  grplmulf1o  13859  grpinvadd  13863  grpinvsub  13867  grpsubsub4  13878  grppnpcan2  13879  grpnpncan  13880  dfgrp3mlem  13883  dfgrp3m  13884  grplactcnv  13887  imasgrp2  13893  mhmlem  13897  mhmid  13898  mhmmnd  13899  mulgnnp1  13913  mulg2  13914  mulgnn0p1  13916  mulgsubcl  13919  mulgneg  13923  mulgaddcomlem  13928  mulgaddcom  13929  mulgz  13933  mulgnn0dir  13935  mulgdirlem  13936  mulgdir  13937  mulgneg2  13939  mulgnnass  13940  mulgnn0ass  13941  mulgass  13942  mulgassr  13943  mulgmodid  13944  mulgsubdir  13945  submmulg  13949  isnsg3  13990  nmzsubg  13993  ssnmz  13994  0nsg  13997  eqger  14007  eqgid  14009  eqgcpbl  14011  ghmlin  14031  ghmmulg  14039  ghmnsgima  14051  ghmnsgpreima  14052  conjghm  14059  conjnmz  14062  ablsub2inv  14095  abladdsub4  14098  abladdsub  14099  ablpncan2  14100  ablpnpcan  14104  ablnncan  14105  ablnnncan1  14108  gzsumconst  14123  gzsumsnfd  14127  gzsumsplit0  14128  gzsumshift  14129  gzsumgsum  14135  gsummptfidmadd  14141  gsumconstcmn  14146  prdssgrpd  14171  prdsidlem  14173  prdsmndd  14174  prdsinvlem  14176  mgpress  14208  rngass  14216  rngdi  14217  rngdir  14218  rnglz  14222  rngmneg1  14224  rngsubdir  14229  rngpropd  14232  imasrng  14233  srgass  14252  srgmulgass  14270  srgpcomp  14271  srgpcompp  14272  srgpcomppsc  14273  ringpropd  14319  ringlz  14324  ring1eq0  14329  ringnegl  14332  ringmneg1  14334  ringsubdir  14338  mulgass2  14339  ring1  14340  imasring  14345  opprrng  14358  opprring  14360  unitgrp  14399  dvrcan1  14423  rdivmuldivd  14427  subrginv  14521  resrhm  14532  unitrrg  14552  aprlring  14576  islmod  14603  lmodlema  14604  islmodd  14605  lmod0vs  14633  lmodvs0  14634  lmodvsmmulgdi  14635  lmodvneg1  14642  lmodvsneg  14643  lmodsubvs  14655  lmodsubdi  14656  lmodsubdir  14657  lmodprop2d  14660  rmodislmodlem  14662  rmodislmod  14663  lsssetm  14668  islssmd  14671  lssclg  14676  lssvacl  14677  lss1d  14695  lsspropdg  14743  sraval  14749  rnglidlmcl  14792  znunit  14969  mplsubgfilemcl  15016  resttop  15197  restco  15201  restin  15203  lmfval  15220  cnprcl2k  15233  txrest  15303  txdis1cn  15305  cnmpt2res  15324  psmettri2  15355  psmettri  15357  xmettri2  15388  xmettri  15399  mettri  15400  metrtri  15404  blvalps  15415  blval  15416  xblss2  15432  blhalf  15435  comet  15526  xmetxp  15534  txmetcnp  15545  cnmet  15557  ioo2bl  15578  ivthreinc  15672  limcmpted  15690  limcimolemlt  15691  cnplimclemr  15696  limccnp2cntop  15704  reldvg  15706  dvfvalap  15708  dvidlemap  15718  dvidrelem  15719  dvidsslem  15720  dvconst  15721  dvconstre  15723  dvconstss  15725  dvcnp2cntop  15726  dvaddxxbr  15728  dvmulxxbr  15729  dvcoapbr  15734  dvcjbr  15735  dvexp  15738  dvrecap  15740  dvmptcmulcn  15748  dveflem  15753  plyval  15759  elply2  15762  elplyr  15767  elplyd  15768  ply1termlem  15769  plyaddlem1  15774  plymullem1  15775  plycoeid3  15784  plycjlemc  15787  dvply1  15792  sin0pilem1  15808  sinperlem  15835  ptolemy  15851  tangtx  15865  abssinper  15873  reexplog  15898  relogexp  15899  cxprec  15938  rpdivcxp  15939  cxpmul  15940  rpabscxpbnd  15968  rplogbval  15973  rplogbreexp  15981  rprelogbmul  15983  logbrec  15988  logbgcd1irraplemap  15997  binom4  16007  pellexlem2  16009  pellexlem3  16010  wilthlem1  16011  mpodvdsmulf1o  16021  sgmppw  16023  0sgmppw  16024  1sgmprm  16025  1sgm2ppw  16026  perfectlem1  16030  perfectlem2  16031  perfect  16032  lgslem1  16036  lgslem4  16039  lgsval  16040  lgsfvalg  16041  lgsval2lem  16046  lgsval4lem  16047  lgsvalmod  16055  lgsneg  16060  lgsneg1  16061  lgsmod  16062  lgsdilem  16063  lgsdir2lem4  16067  lgsdir2  16069  lgsdirprm  16070  lgsdir  16071  lgsne0  16074  lgssq  16076  lgssq2  16077  lgsmulsqcoprm  16082  lgsdirnn0  16083  lgsdinn0  16084  gausslemma2dlem1a  16094  gausslemma2dlem4  16100  gausslemma2dlem5a  16101  gausslemma2dlem5  16102  gausslemma2dlem6  16103  gausslemma2dlem7  16104  gausslemma2d  16105  lgseisenlem1  16106  lgseisenlem2  16107  lgseisenlem3  16108  lgseisenlem4  16109  lgseisen  16110  lgsquadlem1  16113  lgsquadlem2  16114  lgsquad2lem1  16117  lgsquad2lem2  16118  lgsquad3  16120  m1lgs  16121  2lgslem1a  16124  2lgslem1c  16126  2lgslem3a  16129  2lgslem3b  16130  2lgslem3c  16131  2lgslem3d  16132  2lgslem3a1  16133  2lgslem3b1  16134  2lgslem3c1  16135  2lgslem3d1  16136  2lgsoddprmlem1  16141  2lgsoddprmlem2  16142  2lgsoddprmlem3  16147  2sqlem1  16150  2sqlem2  16151  mul2sq  16152  2sqlem3  16153  2sqlem4  16154  2sqlem8  16159  2sqlem9  16160  2sqlem10  16161  vdegp1bid  16473  uspgr2wlkeqi  16525  isclwwlk  16552  clwwlkccatlem  16558  clwwlknonex2  16597  repiecele0  16983  repiecege0  16984  repiecef  16985  trilpolemeq1  16997  trilpolemlt1  16998  trirec0xor  17002  apdifflemf  17003  apdiff  17005  qdiff  17006