Theorem oveq1d 5933

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 5925	. 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 5918

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 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921

This theorem is referenced by:  fvoveq1d  5940  csbov2g  5959  caovassg  6077  caovdig  6093  caovdirg  6096  caov12d  6100  caov31d  6101  caov411d  6104  caofinvl  6155  omsuc  6525  nnmsucr  6541  nnm1  6578  nnm2  6579  ecovass  6698  ecoviass  6699  ecovdi  6700  ecovidi  6701  addasspig  7390  mulasspig  7392  mulpipq2  7431  distrnqg  7447  ltsonq  7458  ltanqg  7460  ltmnqg  7461  ltexnqq  7468  archnqq  7477  prarloclemarch2  7479  enq0sym  7492  addnq0mo  7507  mulnq0mo  7508  addnnnq0  7509  nqpnq0nq  7513  nq0m0r  7516  nq0a0  7517  nnanq0  7518  distrnq0  7519  addassnq0  7522  addpinq1  7524  prarloclemlo  7554  prarloclem3  7557  prarloclem5  7560  prarloclemcalc  7562  addnqprllem  7587  addnqprulem  7588  appdivnq  7623  recexprlem1ssl  7693  recexprlem1ssu  7694  ltmprr  7702  cauappcvgprlemladdru  7716  cauappcvgprlem1  7719  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemcl  7736  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprlem1  7739  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemexb  7767  caucvgprprlem1  7769  addcmpblnr  7799  mulcmpblnrlemg  7800  addsrmo  7803  mulsrmo  7804  addsrpr  7805  mulsrpr  7806  ltsrprg  7807  1idsr  7828  pn0sr  7831  recexgt0sr  7833  mulgt0sr  7838  srpospr  7843  prsradd  7846  caucvgsrlemfv  7851  caucvgsrlemcau  7853  caucvgsrlemgt1  7855  caucvgsrlemoffval  7856  caucvgsrlemoffcau  7858  caucvgsrlemoffres  7860  caucvgsrlembnd  7861  caucvgsr  7862  map2psrprg  7865  pitonnlem1p1  7906  pitonnlem2  7907  pitonn  7908  recidpirqlemcalc  7917  ax1rid  7937  axrnegex  7939  axcnre  7941  recriota  7950  nntopi  7954  axcaucvglemval  7957  axcaucvglemcau  7958  axcaucvglemres  7959  mul12  8148  mul4  8151  muladd11  8152  readdcan  8159  muladd11r  8175  add12  8177  cnegex  8197  addcan  8199  negeu  8210  pncan2  8226  addsubass  8229  addsub  8230  2addsub  8233  addsubeq4  8234  subid  8238  subid1  8239  npncan  8240  nppcan  8241  nnpcan  8242  nnncan1  8255  npncan3  8257  pnpcan  8258  pnncan  8260  ppncan  8261  addsub4  8262  negsub  8267  subneg  8268  subeqxfrd  8382  mvlraddd  8383  mvlladdd  8384  mvrraddd  8385  subaddeqd  8388  ine0  8413  mulneg1  8414  ltadd2  8438  apreap  8606  cru  8621  recexap  8672  mulcanapd  8680  div23ap  8710  div13ap  8712  divmulassap  8714  divmulasscomap  8715  divcanap4  8718  muldivdirap  8726  divsubdirap  8727  divmuldivap  8731  divdivdivap  8732  divcanap5  8733  divmul13ap  8734  divmuleqap  8736  divdiv32ap  8739  divcanap7  8740  dmdcanap  8741  divdivap1  8742  divdivap2  8743  divadddivap  8746  divsubdivap  8747  conjmulap  8748  divneg2ap  8755  subrecap  8858  mvllmulapd  8861  lt2mul2div  8898  nndivtr  9024  2halves  9211  halfaddsub  9216  subhalfhalf  9217  avgle1  9223  avgle2  9224  div4p1lem1div2  9236  un0addcl  9273  un0mulcl  9274  peano2z  9353  zneo  9418  nneoor  9419  nneo  9420  zeo  9422  zeo2  9423  deceq1  9452  qreccl  9707  xaddcom  9927  xnegdi  9934  xaddass  9935  xaddass2  9936  xpncan  9937  xleadd1a  9939  xltadd1  9942  xposdif  9948  xadd4d  9951  lincmb01cmp  10069  iccf1o  10070  fz0to4untppr  10190  fzosubel3  10263  qavgle  10327  2tnp1ge0ge0  10370  fldiv4p1lem1div2  10374  fldiv4lem1div2  10376  ceilqm1lt  10383  flqdiv  10392  modqlt  10404  modqdiffl  10406  modqcyc2  10431  modqaddabs  10433  mulqaddmodid  10435  mulp1mod1  10436  modqmuladd  10437  modqmuladdnn0  10439  qnegmod  10440  addmodid  10443  addmodidr  10444  modqadd2mod  10445  modqm1p1mod0  10446  modqmul12d  10449  modqnegd  10450  modqadd12d  10451  modqsub12d  10452  q2submod  10456  modqmulmodr  10461  modqaddmulmod  10462  modqsubdir  10464  modfzo0difsn  10466  modsumfzodifsn  10467  addmodlteq  10469  frecuzrdgsuc  10485  frecfzennn  10497  iseqovex  10529  seq3-1p  10561  seq3caopr2  10564  seqcaopr2g  10565  seq3caopr  10566  seqcaoprg  10567  seqf1oglem2a  10589  seqf1oglem1  10590  seqf1oglem2  10591  seq3id  10596  seq3homo  10598  seq3z  10599  seqhomog  10601  seqfeq4g  10602  expp1  10617  exprecap  10651  expaddzaplem  10653  expmulzap  10656  expdivap  10661  sqval  10668  sqsubswap  10670  sqdividap  10675  subsq  10717  subsq2  10718  binom2  10722  binom2sub  10724  mulbinom2  10727  binom3  10728  zesq  10729  bernneq2  10732  modqexp  10737  sqoddm1div8  10764  mulsubdivbinom2ap  10782  nn0opthlem1d  10791  nn0opthd  10793  nn0opth2d  10794  facp1  10801  facdiv  10809  facndiv  10810  faclbnd  10812  faclbnd2  10813  faclbnd3  10814  bcval  10820  bccmpl  10825  bcm1k  10831  bcp1n  10832  bcp1nk  10833  bcval5  10834  bcp1m1  10836  bcpasc  10837  bcn2m1  10840  hashprg  10879  hashdifpr  10891  hashfzo  10893  hashfzp1  10895  hashfz0  10896  hashxp  10897  zfz1isolemsplit  10909  zfz1isolem1  10911  seq3coll  10913  reval  10993  crre  11001  remim  11004  remul2  11017  immul2  11024  imval2  11038  cjdivap  11053  caucvgre  11125  cvg1nlemcau  11128  cvg1nlemres  11129  resqrexlemp1rp  11150  resqrexlemfp1  11153  resqrexlemover  11154  resqrexlemcalc1  11158  resqrexlemcalc3  11160  resqrexlemnm  11162  resqrexlemoverl  11165  resqrexlemglsq  11166  resqrexlemga  11167  resqrexlemsqa  11168  resqrexlemex  11169  resqrex  11170  sqrtdiv  11186  absvalsq  11197  absreimsq  11211  absdivap  11214  cau3lem  11258  maxabslemlub  11351  maxabslemval  11352  max0addsup  11363  minabs  11379  bdtrilem  11382  bdtri  11383  xrmaxaddlem  11403  xrmaxadd  11404  xrbdtri  11419  clim  11424  clim2  11426  climshftlemg  11445  climshft2  11449  climcn1  11451  climcn2  11452  subcn2  11454  reccn2ap  11456  climmulc2  11474  climsubc2  11476  clim2ser  11480  iser3shft  11489  climcau  11490  serf0  11495  fzosump1  11560  fsum1p  11561  fsump1  11563  sumsplitdc  11575  fsump1i  11576  mptfzshft  11585  fisum0diag2  11590  fsumconst  11597  fsumdifsnconst  11598  modfsummodlemstep  11600  modfsummod  11601  telfsumo  11609  fsumparts  11613  fsumrelem  11614  hash2iun1dif1  11623  binomlem  11626  binom  11627  binom1p  11628  binom1dif  11630  bcxmas  11632  isumsplit  11634  isum1p  11635  arisum  11641  arisum2  11642  trireciplem  11643  geoserap  11650  geolim  11654  geolim2  11655  georeclim  11656  geo2sum  11657  geoisum1  11662  cvgratnnlemseq  11669  cvgratnnlemsumlt  11671  cvgratnnlemfm  11672  cvgratz  11675  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  fprod1p  11742  fprodp1  11743  fprodcl2lem  11748  fprodfac  11758  fprodeq0  11760  fprodconst  11763  fprodrec  11772  fprodsplit1f  11777  fprodmodd  11784  efcllemp  11801  ef0lem  11803  efval  11804  esum  11805  ege2le3  11814  efaddlem  11817  efsep  11834  effsumlt  11835  eft0val  11836  efgt1p2  11838  efgt1p  11839  sinval  11845  cosval  11846  resinval  11858  recosval  11859  efi4p  11860  resin4p  11861  recos4p  11862  sinneg  11869  cosneg  11870  efival  11875  sinadd  11879  cosadd  11880  tanaddap  11882  sinmul  11887  cosmul  11888  cos2t  11893  cos2tsin  11894  ef01bndlem  11899  absefib  11914  demoivre  11916  demoivreALT  11917  eirraplem  11920  p1modz1  11937  dvdsmodexp  11938  moddvds  11942  mulmoddvds  12005  3dvds2dec  12007  zeo3  12009  odd2np1lem  12013  odd2np1  12014  oexpneg  12018  2tp1odd  12025  ltoddhalfle  12034  opoe  12036  opeo  12038  omeo  12039  m1expo  12041  m1exp1  12042  nn0o1gt2  12046  nn0o  12048  divalglemnn  12059  divalglemqt  12060  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  flodddiv4  12075  flodddiv4t2lthalf  12078  gcdaddm  12121  bezoutlemnewy  12133  bezoutlema  12136  bezoutlemb  12137  bezoutlemex  12138  bezoutlemaz  12140  mulgcd  12153  gcddiv  12156  gcdmultiplez  12158  rpmulgcd  12163  rplpwr  12164  uzwodc  12174  lcmgcdlem  12215  lcmgcd  12216  divgcdcoprmex  12240  cncongr2  12242  prmexpb  12289  rpexp  12291  rpexp1i  12292  sqrt2irrlem  12299  oddpwdclemxy  12307  oddpwdclemndvds  12309  sqpweven  12313  2sqpwodd  12314  sqne2sq  12315  qmuldeneqnum  12333  nn0gcdsq  12338  zgcdsq  12339  numdensq  12340  dfphi2  12358  phiprmpw  12360  phiprm  12361  eulerthlema  12368  eulerthlemh  12369  eulerthlemth  12370  fermltl  12372  prmdiv  12373  prmdiveq  12374  prmdivdiv  12375  hashgcdlem  12376  odzval  12379  odzcllem  12380  odzdvds  12383  vfermltl  12389  powm2modprm  12390  reumodprminv  12391  modprm0  12392  nnnn0modprm0  12393  modprmn0modprm0  12394  coprimeprodsq  12395  coprimeprodsq2  12396  pythagtriplem1  12403  pythagtriplem3  12405  pythagtriplem4  12406  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem15  12416  pythagtriplem16  12417  pythagtriplem17  12418  pythagtriplem18  12419  pceu  12433  pczpre  12435  pcdiv  12440  pcqdiv  12445  pcrec  12446  pczndvds  12454  pcneg  12463  pc2dvds  12468  pcprmpw2  12471  pcaddlem  12477  pcadd  12478  fldivp1  12486  pockthlem  12494  pockthi  12496  4sqlem5  12520  4sqlem9  12524  4sqlem10  12525  4sqlem2  12527  4sqlem3  12528  4sqlem4  12530  mul4sqlem  12531  4sqlem11  12539  4sqlem12  12540  4sqlem14  12542  4sqlem15  12543  4sqlem17  12545  4sqlem19  12547  ennnfonelemkh  12569  ennnfonelemhf1o  12570  setscomd  12659  ressressg  12693  qusex  12908  qusin  12909  grpinvalem  12968  grpinva  12969  grprida  12970  gsumsplit1r  12981  isnsgrp  12989  sgrpass  12991  sgrp1  12994  sgrppropd  12996  mnd12g  13009  mndpropd  13021  mhmex  13034  mhmlin  13039  grprcan  13109  grpinvid1  13124  isgrpinv  13126  grplcan  13134  grpasscan1  13135  grplmulf1o  13146  grpinvadd  13150  grpinvsub  13154  grpsubsub4  13165  grppnpcan2  13166  grpnpncan  13167  dfgrp3mlem  13170  dfgrp3m  13171  grplactcnv  13174  imasgrp2  13180  mhmlem  13184  mhmid  13185  mhmmnd  13186  mulgnnp1  13200  mulg2  13201  mulgnn0p1  13203  mulgsubcl  13206  mulgneg  13210  mulgaddcomlem  13215  mulgaddcom  13216  mulgz  13220  mulgnn0dir  13222  mulgdirlem  13223  mulgdir  13224  mulgneg2  13226  mulgnnass  13227  mulgnn0ass  13228  mulgass  13229  mulgassr  13230  mulgmodid  13231  mulgsubdir  13232  submmulg  13236  isnsg3  13277  nmzsubg  13280  ssnmz  13281  0nsg  13284  eqger  13294  eqgid  13296  eqgcpbl  13298  ghmlin  13318  ghmmulg  13326  ghmnsgima  13338  ghmnsgpreima  13339  conjghm  13346  conjnmz  13349  ablsub2inv  13381  abladdsub4  13384  abladdsub  13385  ablpncan2  13386  ablpnpcan  13390  ablnncan  13391  ablnnncan1  13394  gsumfzconst  13411  gsumfzsnfd  13415  mgpress  13427  rngass  13435  rngdi  13436  rngdir  13437  rnglz  13441  rngmneg1  13443  rngsubdir  13448  rngpropd  13451  imasrng  13452  srgass  13467  srgmulgass  13485  srgpcomp  13486  srgpcompp  13487  srgpcomppsc  13488  ringpropd  13534  ringlz  13539  ring1eq0  13544  ringnegl  13547  ringmneg1  13549  ringsubdir  13553  mulgass2  13554  ring1  13555  imasring  13560  opprrng  13573  opprring  13575  unitgrp  13612  dvrcan1  13636  rdivmuldivd  13640  subrginv  13733  resrhm  13744  unitrrg  13763  islmod  13787  lmodlema  13788  islmodd  13789  lmod0vs  13817  lmodvs0  13818  lmodvsmmulgdi  13819  lmodvneg1  13826  lmodvsneg  13827  lmodsubvs  13839  lmodsubdi  13840  lmodsubdir  13841  lmodprop2d  13844  rmodislmodlem  13846  rmodislmod  13847  lsssetm  13852  islssmd  13855  lssclg  13860  lssvacl  13861  lss1d  13879  lsspropdg  13927  sraval  13933  rnglidlmcl  13976  gsumfzfsumlemm  14075  znunit  14147  resttop  14338  restco  14342  restin  14344  lmfval  14360  cnprcl2k  14374  txrest  14444  txdis1cn  14446  cnmpt2res  14465  psmettri2  14496  psmettri  14498  xmettri2  14529  xmettri  14540  mettri  14541  metrtri  14545  blvalps  14556  blval  14557  xblss2  14573  blhalf  14576  comet  14667  xmetxp  14675  txmetcnp  14686  cnmet  14698  ioo2bl  14711  ivthreinc  14799  limcmpted  14817  limcimolemlt  14818  cnplimclemr  14823  limccnp2cntop  14831  reldvg  14833  dvfvalap  14835  dvidlemap  14845  dvconst  14846  dvcnp2cntop  14848  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvcjbr  14857  dvexp  14860  dvrecap  14862  dvmptcmulcn  14868  dveflem  14872  plyval  14878  elply2  14881  elplyr  14886  elplyd  14887  ply1termlem  14888  plyaddlem1  14893  plymullem1  14894  sin0pilem1  14916  sinperlem  14943  ptolemy  14959  tangtx  14973  abssinper  14981  reexplog  15006  relogexp  15007  cxprec  15045  rpdivcxp  15046  cxpmul  15047  rpabscxpbnd  15073  rplogbval  15077  rplogbreexp  15085  rprelogbmul  15087  logbrec  15092  logbgcd1irraplemap  15101  binom4  15111  wilthlem1  15112  lgslem1  15116  lgslem4  15119  lgsval  15120  lgsfvalg  15121  lgsval2lem  15126  lgsval4lem  15127  lgsvalmod  15135  lgsneg  15140  lgsneg1  15141  lgsmod  15142  lgsdilem  15143  lgsdir2lem4  15147  lgsdir2  15149  lgsdirprm  15150  lgsdir  15151  lgsne0  15154  lgssq  15156  lgssq2  15157  lgsmulsqcoprm  15162  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem1a  15174  gausslemma2dlem4  15180  gausslemma2dlem5a  15181  gausslemma2dlem5  15182  gausslemma2dlem6  15183  gausslemma2dlem7  15184  gausslemma2d  15185  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgseisen  15190  lgsquadlem1  15191  m1lgs  15192  2lgsoddprmlem1  15193  2lgsoddprmlem2  15194  2lgsoddprmlem3  15199  2sqlem1  15201  2sqlem2  15202  mul2sq  15203  2sqlem3  15204  2sqlem4  15205  2sqlem8  15210  2sqlem9  15211  2sqlem10  15212  trilpolemeq1  15530  trilpolemlt1  15531  trirec0xor  15535  apdifflemf  15536  apdiff  15538