Theorem oveq1d 5934

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 5926	. 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 1364  (class class class)co 5919

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922

This theorem is referenced by:  fvoveq1d  5941  csbov2g  5960  caovassg  6079  caovdig  6095  caovdirg  6098  caov12d  6102  caov31d  6103  caov411d  6106  caofinvl  6157  omsuc  6527  nnmsucr  6543  nnm1  6580  nnm2  6581  ecovass  6700  ecoviass  6701  ecovdi  6702  ecovidi  6703  addasspig  7392  mulasspig  7394  mulpipq2  7433  distrnqg  7449  ltsonq  7460  ltanqg  7462  ltmnqg  7463  ltexnqq  7470  archnqq  7479  prarloclemarch2  7481  enq0sym  7494  addnq0mo  7509  mulnq0mo  7510  addnnnq0  7511  nqpnq0nq  7515  nq0m0r  7518  nq0a0  7519  nnanq0  7520  distrnq0  7521  addassnq0  7524  addpinq1  7526  prarloclemlo  7556  prarloclem3  7559  prarloclem5  7562  prarloclemcalc  7564  addnqprllem  7589  addnqprulem  7590  appdivnq  7625  recexprlem1ssl  7695  recexprlem1ssu  7696  ltmprr  7704  cauappcvgprlemladdru  7718  cauappcvgprlem1  7721  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemcl  7738  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem1  7741  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemexb  7769  caucvgprprlem1  7771  addcmpblnr  7801  mulcmpblnrlemg  7802  addsrmo  7805  mulsrmo  7806  addsrpr  7807  mulsrpr  7808  ltsrprg  7809  1idsr  7830  pn0sr  7833  recexgt0sr  7835  mulgt0sr  7840  srpospr  7845  prsradd  7848  caucvgsrlemfv  7853  caucvgsrlemcau  7855  caucvgsrlemgt1  7857  caucvgsrlemoffval  7858  caucvgsrlemoffcau  7860  caucvgsrlemoffres  7862  caucvgsrlembnd  7863  caucvgsr  7864  map2psrprg  7867  pitonnlem1p1  7908  pitonnlem2  7909  pitonn  7910  recidpirqlemcalc  7919  ax1rid  7939  axrnegex  7941  axcnre  7943  recriota  7952  nntopi  7956  axcaucvglemval  7959  axcaucvglemcau  7960  axcaucvglemres  7961  mul12  8150  mul4  8153  muladd11  8154  readdcan  8161  muladd11r  8177  add12  8179  cnegex  8199  addcan  8201  negeu  8212  pncan2  8228  addsubass  8231  addsub  8232  2addsub  8235  addsubeq4  8236  subid  8240  subid1  8241  npncan  8242  nppcan  8243  nnpcan  8244  nnncan1  8257  npncan3  8259  pnpcan  8260  pnncan  8262  ppncan  8263  addsub4  8264  negsub  8269  subneg  8270  subeqxfrd  8384  mvlraddd  8385  mvlladdd  8386  mvrraddd  8387  subaddeqd  8390  ine0  8415  mulneg1  8416  ltadd2  8440  apreap  8608  cru  8623  recexap  8674  mulcanapd  8682  div23ap  8712  div13ap  8714  divmulassap  8716  divmulasscomap  8717  divcanap4  8720  muldivdirap  8728  divsubdirap  8729  divmuldivap  8733  divdivdivap  8734  divcanap5  8735  divmul13ap  8736  divmuleqap  8738  divdiv32ap  8741  divcanap7  8742  dmdcanap  8743  divdivap1  8744  divdivap2  8745  divadddivap  8748  divsubdivap  8749  conjmulap  8750  divneg2ap  8757  subrecap  8860  mvllmulapd  8863  lt2mul2div  8900  nndivtr  9026  2halves  9214  halfaddsub  9219  subhalfhalf  9220  avgle1  9226  avgle2  9227  div4p1lem1div2  9239  un0addcl  9276  un0mulcl  9277  peano2z  9356  zneo  9421  nneoor  9422  nneo  9423  zeo  9425  zeo2  9426  deceq1  9455  qreccl  9710  xaddcom  9930  xnegdi  9937  xaddass  9938  xaddass2  9939  xpncan  9940  xleadd1a  9942  xltadd1  9945  xposdif  9951  xadd4d  9954  lincmb01cmp  10072  iccf1o  10073  fz0to4untppr  10193  fzosubel3  10266  qavgle  10330  2tnp1ge0ge0  10373  fldiv4p1lem1div2  10377  fldiv4lem1div2  10379  ceilqm1lt  10386  flqdiv  10395  modqlt  10407  modqdiffl  10409  modqcyc2  10434  modqaddabs  10436  mulqaddmodid  10438  mulp1mod1  10439  modqmuladd  10440  modqmuladdnn0  10442  qnegmod  10443  addmodid  10446  addmodidr  10447  modqadd2mod  10448  modqm1p1mod0  10449  modqmul12d  10452  modqnegd  10453  modqadd12d  10454  modqsub12d  10455  q2submod  10459  modqmulmodr  10464  modqaddmulmod  10465  modqsubdir  10467  modfzo0difsn  10469  modsumfzodifsn  10470  addmodlteq  10472  frecuzrdgsuc  10488  frecfzennn  10500  iseqovex  10532  seq3-1p  10564  seq3caopr2  10567  seqcaopr2g  10568  seq3caopr  10569  seqcaoprg  10570  seqf1oglem2a  10592  seqf1oglem1  10593  seqf1oglem2  10594  seq3id  10599  seq3homo  10601  seq3z  10602  seqhomog  10604  seqfeq4g  10605  expp1  10620  exprecap  10654  expaddzaplem  10656  expmulzap  10659  expdivap  10664  sqval  10671  sqsubswap  10673  sqdividap  10678  subsq  10720  subsq2  10721  binom2  10725  binom2sub  10727  mulbinom2  10730  binom3  10731  zesq  10732  bernneq2  10735  modqexp  10740  sqoddm1div8  10767  mulsubdivbinom2ap  10785  nn0opthlem1d  10794  nn0opthd  10796  nn0opth2d  10797  facp1  10804  facdiv  10812  facndiv  10813  faclbnd  10815  faclbnd2  10816  faclbnd3  10817  bcval  10823  bccmpl  10828  bcm1k  10834  bcp1n  10835  bcp1nk  10836  bcval5  10837  bcp1m1  10839  bcpasc  10840  bcn2m1  10843  hashprg  10882  hashdifpr  10894  hashfzo  10896  hashfzp1  10898  hashfz0  10899  hashxp  10900  zfz1isolemsplit  10912  zfz1isolem1  10914  seq3coll  10916  reval  10996  crre  11004  remim  11007  remul2  11020  immul2  11027  imval2  11041  cjdivap  11056  caucvgre  11128  cvg1nlemcau  11131  cvg1nlemres  11132  resqrexlemp1rp  11153  resqrexlemfp1  11156  resqrexlemover  11157  resqrexlemcalc1  11161  resqrexlemcalc3  11163  resqrexlemnm  11165  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemga  11170  resqrexlemsqa  11171  resqrexlemex  11172  resqrex  11173  sqrtdiv  11189  absvalsq  11200  absreimsq  11214  absdivap  11217  cau3lem  11261  maxabslemlub  11354  maxabslemval  11355  max0addsup  11366  minabs  11382  bdtrilem  11385  bdtri  11386  xrmaxaddlem  11406  xrmaxadd  11407  xrbdtri  11422  clim  11427  clim2  11429  climshftlemg  11448  climshft2  11452  climcn1  11454  climcn2  11455  subcn2  11457  reccn2ap  11459  climmulc2  11477  climsubc2  11479  clim2ser  11483  iser3shft  11492  climcau  11493  serf0  11498  fzosump1  11563  fsum1p  11564  fsump1  11566  sumsplitdc  11578  fsump1i  11579  mptfzshft  11588  fisum0diag2  11593  fsumconst  11600  fsumdifsnconst  11601  modfsummodlemstep  11603  modfsummod  11604  telfsumo  11612  fsumparts  11616  fsumrelem  11617  hash2iun1dif1  11626  binomlem  11629  binom  11630  binom1p  11631  binom1dif  11633  bcxmas  11635  isumsplit  11637  isum1p  11638  arisum  11644  arisum2  11645  trireciplem  11646  geoserap  11653  geolim  11657  geolim2  11658  georeclim  11659  geo2sum  11660  geoisum1  11665  cvgratnnlemseq  11672  cvgratnnlemsumlt  11674  cvgratnnlemfm  11675  cvgratz  11678  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  fprod1p  11745  fprodp1  11746  fprodcl2lem  11751  fprodfac  11761  fprodeq0  11763  fprodconst  11766  fprodrec  11775  fprodsplit1f  11780  fprodmodd  11787  efcllemp  11804  ef0lem  11806  efval  11807  esum  11808  ege2le3  11817  efaddlem  11820  efsep  11837  effsumlt  11838  eft0val  11839  efgt1p2  11841  efgt1p  11842  sinval  11848  cosval  11849  resinval  11861  recosval  11862  efi4p  11863  resin4p  11864  recos4p  11865  sinneg  11872  cosneg  11873  efival  11878  sinadd  11882  cosadd  11883  tanaddap  11885  sinmul  11890  cosmul  11891  cos2t  11896  cos2tsin  11897  ef01bndlem  11902  absefib  11917  demoivre  11919  demoivreALT  11920  eirraplem  11923  p1modz1  11940  dvdsmodexp  11941  moddvds  11945  mulmoddvds  12008  3dvds2dec  12010  zeo3  12012  odd2np1lem  12016  odd2np1  12017  oexpneg  12021  2tp1odd  12028  ltoddhalfle  12037  opoe  12039  opeo  12041  omeo  12042  m1expo  12044  m1exp1  12045  nn0o1gt2  12049  nn0o  12051  divalglemnn  12062  divalglemqt  12063  divalglemeunn  12065  divalglemex  12066  divalglemeuneg  12067  flodddiv4  12078  flodddiv4t2lthalf  12081  gcdaddm  12124  bezoutlemnewy  12136  bezoutlema  12139  bezoutlemb  12140  bezoutlemex  12141  bezoutlemaz  12143  mulgcd  12156  gcddiv  12159  gcdmultiplez  12161  rpmulgcd  12166  rplpwr  12167  uzwodc  12177  lcmgcdlem  12218  lcmgcd  12219  divgcdcoprmex  12243  cncongr2  12245  prmexpb  12292  rpexp  12294  rpexp1i  12295  sqrt2irrlem  12302  oddpwdclemxy  12310  oddpwdclemndvds  12312  sqpweven  12316  2sqpwodd  12317  sqne2sq  12318  qmuldeneqnum  12336  nn0gcdsq  12341  zgcdsq  12342  numdensq  12343  dfphi2  12361  phiprmpw  12363  phiprm  12364  eulerthlema  12371  eulerthlemh  12372  eulerthlemth  12373  fermltl  12375  prmdiv  12376  prmdiveq  12377  prmdivdiv  12378  hashgcdlem  12379  odzval  12382  odzcllem  12383  odzdvds  12386  vfermltl  12392  powm2modprm  12393  reumodprminv  12394  modprm0  12395  nnnn0modprm0  12396  modprmn0modprm0  12397  coprimeprodsq  12398  coprimeprodsq2  12399  pythagtriplem1  12406  pythagtriplem3  12408  pythagtriplem4  12409  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem15  12419  pythagtriplem16  12420  pythagtriplem17  12421  pythagtriplem18  12422  pceu  12436  pczpre  12438  pcdiv  12443  pcqdiv  12448  pcrec  12449  pczndvds  12457  pcneg  12466  pc2dvds  12471  pcprmpw2  12474  pcaddlem  12480  pcadd  12481  fldivp1  12489  pockthlem  12497  pockthi  12499  4sqlem5  12523  4sqlem9  12527  4sqlem10  12528  4sqlem2  12530  4sqlem3  12531  4sqlem4  12533  mul4sqlem  12534  4sqlem11  12542  4sqlem12  12543  4sqlem14  12545  4sqlem15  12546  4sqlem17  12548  4sqlem19  12550  ennnfonelemkh  12572  ennnfonelemhf1o  12573  setscomd  12662  ressressg  12696  qusex  12911  qusin  12912  grpinvalem  12971  grpinva  12972  grprida  12973  gsumsplit1r  12984  isnsgrp  12992  sgrpass  12994  sgrp1  12997  sgrppropd  12999  mnd12g  13012  mndpropd  13024  mhmex  13037  mhmlin  13042  grprcan  13112  grpinvid1  13127  isgrpinv  13129  grplcan  13137  grpasscan1  13138  grplmulf1o  13149  grpinvadd  13153  grpinvsub  13157  grpsubsub4  13168  grppnpcan2  13169  grpnpncan  13170  dfgrp3mlem  13173  dfgrp3m  13174  grplactcnv  13177  imasgrp2  13183  mhmlem  13187  mhmid  13188  mhmmnd  13189  mulgnnp1  13203  mulg2  13204  mulgnn0p1  13206  mulgsubcl  13209  mulgneg  13213  mulgaddcomlem  13218  mulgaddcom  13219  mulgz  13223  mulgnn0dir  13225  mulgdirlem  13226  mulgdir  13227  mulgneg2  13229  mulgnnass  13230  mulgnn0ass  13231  mulgass  13232  mulgassr  13233  mulgmodid  13234  mulgsubdir  13235  submmulg  13239  isnsg3  13280  nmzsubg  13283  ssnmz  13284  0nsg  13287  eqger  13297  eqgid  13299  eqgcpbl  13301  ghmlin  13321  ghmmulg  13329  ghmnsgima  13341  ghmnsgpreima  13342  conjghm  13349  conjnmz  13352  ablsub2inv  13384  abladdsub4  13387  abladdsub  13388  ablpncan2  13389  ablpnpcan  13393  ablnncan  13394  ablnnncan1  13397  gsumfzconst  13414  gsumfzsnfd  13418  mgpress  13430  rngass  13438  rngdi  13439  rngdir  13440  rnglz  13444  rngmneg1  13446  rngsubdir  13451  rngpropd  13454  imasrng  13455  srgass  13470  srgmulgass  13488  srgpcomp  13489  srgpcompp  13490  srgpcomppsc  13491  ringpropd  13537  ringlz  13542  ring1eq0  13547  ringnegl  13550  ringmneg1  13552  ringsubdir  13556  mulgass2  13557  ring1  13558  imasring  13563  opprrng  13576  opprring  13578  unitgrp  13615  dvrcan1  13639  rdivmuldivd  13643  subrginv  13736  resrhm  13747  unitrrg  13766  islmod  13790  lmodlema  13791  islmodd  13792  lmod0vs  13820  lmodvs0  13821  lmodvsmmulgdi  13822  lmodvneg1  13829  lmodvsneg  13830  lmodsubvs  13842  lmodsubdi  13843  lmodsubdir  13844  lmodprop2d  13847  rmodislmodlem  13849  rmodislmod  13850  lsssetm  13855  islssmd  13858  lssclg  13863  lssvacl  13864  lss1d  13882  lsspropdg  13930  sraval  13936  rnglidlmcl  13979  gsumfzfsumlemm  14086  znunit  14158  resttop  14349  restco  14353  restin  14355  lmfval  14371  cnprcl2k  14385  txrest  14455  txdis1cn  14457  cnmpt2res  14476  psmettri2  14507  psmettri  14509  xmettri2  14540  xmettri  14551  mettri  14552  metrtri  14556  blvalps  14567  blval  14568  xblss2  14584  blhalf  14587  comet  14678  xmetxp  14686  txmetcnp  14697  cnmet  14709  ioo2bl  14730  ivthreinc  14824  limcmpted  14842  limcimolemlt  14843  cnplimclemr  14848  limccnp2cntop  14856  reldvg  14858  dvfvalap  14860  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvconst  14873  dvconstre  14875  dvconstss  14877  dvcnp2cntop  14878  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvcjbr  14887  dvexp  14890  dvrecap  14892  dvmptcmulcn  14900  dveflem  14905  plyval  14911  elply2  14914  elplyr  14919  elplyd  14920  ply1termlem  14921  plyaddlem1  14926  plymullem1  14927  plycjlemc  14938  dvply1  14943  sin0pilem1  14957  sinperlem  14984  ptolemy  15000  tangtx  15014  abssinper  15022  reexplog  15047  relogexp  15048  cxprec  15086  rpdivcxp  15087  cxpmul  15088  rpabscxpbnd  15114  rplogbval  15118  rplogbreexp  15126  rprelogbmul  15128  logbrec  15133  logbgcd1irraplemap  15142  binom4  15152  wilthlem1  15153  lgslem1  15157  lgslem4  15160  lgsval  15161  lgsfvalg  15162  lgsval2lem  15167  lgsval4lem  15168  lgsvalmod  15176  lgsneg  15181  lgsneg1  15182  lgsmod  15183  lgsdilem  15184  lgsdir2lem4  15188  lgsdir2  15190  lgsdirprm  15191  lgsdir  15192  lgsne0  15195  lgssq  15197  lgssq2  15198  lgsmulsqcoprm  15203  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem1a  15215  gausslemma2dlem4  15221  gausslemma2dlem5a  15222  gausslemma2dlem5  15223  gausslemma2dlem6  15224  gausslemma2dlem7  15225  gausslemma2d  15226  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem1  15238  lgsquad2lem2  15239  lgsquad3  15241  m1lgs  15242  2lgslem1a  15245  2lgslem1c  15247  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgslem3d1  15257  2lgsoddprmlem1  15262  2lgsoddprmlem2  15263  2lgsoddprmlem3  15268  2sqlem1  15271  2sqlem2  15272  mul2sq  15273  2sqlem3  15274  2sqlem4  15275  2sqlem8  15280  2sqlem9  15281  2sqlem10  15282  trilpolemeq1  15600  trilpolemlt1  15601  trirec0xor  15605  apdifflemf  15606  apdiff  15608