Theorem oveq1d 6016

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 6008	. 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 1395  (class class class)co 6001

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6004

This theorem is referenced by:  fvoveq1d  6023  csbov2g  6043  caovassg  6164  caovdig  6180  caovdirg  6183  caov12d  6187  caov31d  6188  caov411d  6191  caofinvl  6244  omsuc  6618  nnmsucr  6634  nnm1  6671  nnm2  6672  ecovass  6791  ecoviass  6792  ecovdi  6793  ecovidi  6794  isacnm  7385  addasspig  7517  mulasspig  7519  mulpipq2  7558  distrnqg  7574  ltsonq  7585  ltanqg  7587  ltmnqg  7588  ltexnqq  7595  archnqq  7604  prarloclemarch2  7606  enq0sym  7619  addnq0mo  7634  mulnq0mo  7635  addnnnq0  7636  nqpnq0nq  7640  nq0m0r  7643  nq0a0  7644  nnanq0  7645  distrnq0  7646  addassnq0  7649  addpinq1  7651  prarloclemlo  7681  prarloclem3  7684  prarloclem5  7687  prarloclemcalc  7689  addnqprllem  7714  addnqprulem  7715  appdivnq  7750  recexprlem1ssl  7820  recexprlem1ssu  7821  ltmprr  7829  cauappcvgprlemladdru  7843  cauappcvgprlem1  7846  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemcl  7863  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  caucvgprlem1  7866  caucvgprprlemcbv  7874  caucvgprprlemval  7875  caucvgprprlemexb  7894  caucvgprprlem1  7896  addcmpblnr  7926  mulcmpblnrlemg  7927  addsrmo  7930  mulsrmo  7931  addsrpr  7932  mulsrpr  7933  ltsrprg  7934  1idsr  7955  pn0sr  7958  recexgt0sr  7960  mulgt0sr  7965  srpospr  7970  prsradd  7973  caucvgsrlemfv  7978  caucvgsrlemcau  7980  caucvgsrlemgt1  7982  caucvgsrlemoffval  7983  caucvgsrlemoffcau  7985  caucvgsrlemoffres  7987  caucvgsrlembnd  7988  caucvgsr  7989  map2psrprg  7992  pitonnlem1p1  8033  pitonnlem2  8034  pitonn  8035  recidpirqlemcalc  8044  ax1rid  8064  axrnegex  8066  axcnre  8068  recriota  8077  nntopi  8081  axcaucvglemval  8084  axcaucvglemcau  8085  axcaucvglemres  8086  mul12  8275  mul4  8278  muladd11  8279  readdcan  8286  muladd11r  8302  add12  8304  cnegex  8324  addcan  8326  negeu  8337  pncan2  8353  addsubass  8356  addsub  8357  2addsub  8360  addsubeq4  8361  subid  8365  subid1  8366  npncan  8367  nppcan  8368  nnpcan  8369  nnncan1  8382  npncan3  8384  pnpcan  8385  pnncan  8387  ppncan  8388  addsub4  8389  negsub  8394  subneg  8395  subeqxfrd  8509  mvlraddd  8510  mvlladdd  8511  mvrraddd  8512  subaddeqd  8515  ine0  8540  mulneg1  8541  ltadd2  8566  apreap  8734  cru  8749  recexap  8800  mulcanapd  8808  div23ap  8838  div13ap  8840  divmulassap  8842  divmulasscomap  8843  divcanap4  8846  muldivdirap  8854  divsubdirap  8855  divmuldivap  8859  divdivdivap  8860  divcanap5  8861  divmul13ap  8862  divmuleqap  8864  divdiv32ap  8867  divcanap7  8868  dmdcanap  8869  divdivap1  8870  divdivap2  8871  divadddivap  8874  divsubdivap  8875  conjmulap  8876  divneg2ap  8883  subrecap  8986  mvllmulapd  8989  lt2mul2div  9026  nndivtr  9152  2halves  9340  halfaddsub  9345  subhalfhalf  9346  avgle1  9352  avgle2  9353  div4p1lem1div2  9365  un0addcl  9402  un0mulcl  9403  peano2z  9482  zneo  9548  nneoor  9549  nneo  9550  zeo  9552  zeo2  9553  deceq1  9582  qreccl  9837  xaddcom  10057  xnegdi  10064  xaddass  10065  xaddass2  10066  xpncan  10067  xleadd1a  10069  xltadd1  10072  xposdif  10078  xadd4d  10081  lincmb01cmp  10199  iccf1o  10200  fz0to4untppr  10320  fzo0addel  10394  fzosubel3  10402  qavgle  10478  2tnp1ge0ge0  10521  fldiv4p1lem1div2  10525  fldiv4lem1div2  10527  ceilqm1lt  10534  flqdiv  10543  modqlt  10555  modqdiffl  10557  modqcyc2  10582  modqaddabs  10584  mulqaddmodid  10586  mulp1mod1  10587  modqmuladd  10588  modqmuladdnn0  10590  qnegmod  10591  addmodid  10594  addmodidr  10595  modqadd2mod  10596  modqm1p1mod0  10597  modqmul12d  10600  modqnegd  10601  modqadd12d  10602  modqsub12d  10603  q2submod  10607  modqmulmodr  10612  modqaddmulmod  10613  modqsubdir  10615  modfzo0difsn  10617  modsumfzodifsn  10618  addmodlteq  10620  frecuzrdgsuc  10636  frecfzennn  10648  iseqovex  10680  seq3-1p  10712  seq3caopr2  10715  seqcaopr2g  10716  seq3caopr  10717  seqcaoprg  10718  seqf1oglem2a  10740  seqf1oglem1  10741  seqf1oglem2  10742  seq3id  10747  seq3homo  10749  seq3z  10750  seqhomog  10752  seqfeq4g  10753  expp1  10768  exprecap  10802  expaddzaplem  10804  expmulzap  10807  expdivap  10812  sqval  10819  sqsubswap  10821  sqdividap  10826  subsq  10868  subsq2  10869  binom2  10873  binom2sub  10875  mulbinom2  10878  binom3  10879  zesq  10880  bernneq2  10883  modqexp  10888  sqoddm1div8  10915  mulsubdivbinom2ap  10933  nn0opthlem1d  10942  nn0opthd  10944  nn0opth2d  10945  facp1  10952  facdiv  10960  facndiv  10961  faclbnd  10963  faclbnd2  10964  faclbnd3  10965  bcval  10971  bccmpl  10976  bcm1k  10982  bcp1n  10983  bcp1nk  10984  bcval5  10985  bcp1m1  10987  bcpasc  10988  bcn2m1  10991  hashprg  11030  hashdifpr  11042  hashfzo  11044  hashfzp1  11046  hashfz0  11047  hashxp  11048  zfz1isolemsplit  11060  zfz1isolem1  11062  seq3coll  11064  lswwrd  11118  ccatfvalfi  11127  ccatass  11143  lswccatn0lsw  11146  ccatswrd  11202  ccatpfx  11233  swrdpfx  11239  pfxpfx  11240  ccats1pfxeq  11246  wrdeqs1cat  11252  wrdind  11254  wrd2ind  11255  pfxccatpfx2  11269  pfxccatin12d  11277  cats1catd  11300  cats2catd  11301  s2leng  11321  reval  11360  crre  11368  remim  11371  remul2  11384  immul2  11391  imval2  11405  cjdivap  11420  caucvgre  11492  cvg1nlemcau  11495  cvg1nlemres  11496  resqrexlemp1rp  11517  resqrexlemfp1  11520  resqrexlemover  11521  resqrexlemcalc1  11525  resqrexlemcalc3  11527  resqrexlemnm  11529  resqrexlemoverl  11532  resqrexlemglsq  11533  resqrexlemga  11534  resqrexlemsqa  11535  resqrexlemex  11536  resqrex  11537  sqrtdiv  11553  absvalsq  11564  absreimsq  11578  absdivap  11581  cau3lem  11625  maxabslemlub  11718  maxabslemval  11719  max0addsup  11730  minabs  11747  bdtrilem  11750  bdtri  11751  xrmaxaddlem  11771  xrmaxadd  11772  xrbdtri  11787  clim  11792  clim2  11794  climshftlemg  11813  climshft2  11817  climcn1  11819  climcn2  11820  subcn2  11822  reccn2ap  11824  climmulc2  11842  climsubc2  11844  clim2ser  11848  iser3shft  11857  climcau  11858  serf0  11863  fzosump1  11928  fsum1p  11929  fsump1  11931  sumsplitdc  11943  fsump1i  11944  mptfzshft  11953  fisum0diag2  11958  fsumconst  11965  fsumdifsnconst  11966  modfsummodlemstep  11968  modfsummod  11969  telfsumo  11977  fsumparts  11981  fsumrelem  11982  hash2iun1dif1  11991  binomlem  11994  binom  11995  binom1p  11996  binom1dif  11998  bcxmas  12000  isumsplit  12002  isum1p  12003  arisum  12009  arisum2  12010  trireciplem  12011  geoserap  12018  geolim  12022  geolim2  12023  georeclim  12024  geo2sum  12025  geoisum1  12030  cvgratnnlemseq  12037  cvgratnnlemsumlt  12039  cvgratnnlemfm  12040  cvgratz  12043  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  fprod1p  12110  fprodp1  12111  fprodcl2lem  12116  fprodfac  12126  fprodeq0  12128  fprodconst  12131  fprodrec  12140  fprodsplit1f  12145  fprodmodd  12152  efcllemp  12169  ef0lem  12171  efval  12172  esum  12173  ege2le3  12182  efaddlem  12185  efsep  12202  effsumlt  12203  eft0val  12204  efgt1p2  12206  efgt1p  12207  sinval  12213  cosval  12214  resinval  12226  recosval  12227  efi4p  12228  resin4p  12229  recos4p  12230  sinneg  12237  cosneg  12238  efival  12243  sinadd  12247  cosadd  12248  tanaddap  12250  sinmul  12255  cosmul  12256  cos2t  12261  cos2tsin  12262  ef01bndlem  12267  absefib  12282  demoivre  12284  demoivreALT  12285  eirraplem  12288  p1modz1  12305  dvdsmodexp  12306  moddvds  12310  mulmoddvds  12374  3dvds2dec  12377  zeo3  12379  odd2np1lem  12383  odd2np1  12384  oexpneg  12388  2tp1odd  12395  ltoddhalfle  12404  opoe  12406  opeo  12408  omeo  12409  m1expo  12411  m1exp1  12412  nn0o1gt2  12416  nn0o  12418  divalglemnn  12429  divalglemqt  12430  divalglemeunn  12432  divalglemex  12433  divalglemeuneg  12434  flodddiv4  12447  flodddiv4t2lthalf  12450  bitsp1o  12464  bitsmod  12467  bitsinv1lem  12472  gcdaddm  12505  bezoutlemnewy  12517  bezoutlema  12520  bezoutlemb  12521  bezoutlemex  12522  bezoutlemaz  12524  mulgcd  12537  gcddiv  12540  gcdmultiplez  12542  rpmulgcd  12547  rplpwr  12548  uzwodc  12558  lcmgcdlem  12599  lcmgcd  12600  divgcdcoprmex  12624  cncongr2  12626  prmexpb  12673  rpexp  12675  rpexp1i  12676  sqrt2irrlem  12683  oddpwdclemxy  12691  oddpwdclemndvds  12693  sqpweven  12697  2sqpwodd  12698  sqne2sq  12699  qmuldeneqnum  12717  nn0gcdsq  12722  zgcdsq  12723  numdensq  12724  dfphi2  12742  phiprmpw  12744  phiprm  12745  eulerthlema  12752  eulerthlemh  12753  eulerthlemth  12754  fermltl  12756  prmdiv  12757  prmdiveq  12758  prmdivdiv  12759  hashgcdlem  12760  odzval  12764  odzcllem  12765  odzdvds  12768  vfermltl  12774  powm2modprm  12775  reumodprminv  12776  modprm0  12777  nnnn0modprm0  12778  modprmn0modprm0  12779  coprimeprodsq  12780  coprimeprodsq2  12781  pythagtriplem1  12788  pythagtriplem3  12790  pythagtriplem4  12791  pythagtriplem6  12793  pythagtriplem7  12794  pythagtriplem12  12798  pythagtriplem14  12800  pythagtriplem15  12801  pythagtriplem16  12802  pythagtriplem17  12803  pythagtriplem18  12804  pceu  12818  pczpre  12820  pcdiv  12825  pcqdiv  12830  pcrec  12831  pczndvds  12839  pcneg  12848  pc2dvds  12853  pcprmpw2  12856  pcaddlem  12862  pcadd  12863  fldivp1  12871  pockthlem  12879  pockthi  12881  4sqlem5  12905  4sqlem9  12909  4sqlem10  12910  4sqlem2  12912  4sqlem3  12913  4sqlem4  12915  mul4sqlem  12916  4sqlem11  12924  4sqlem12  12925  4sqlem14  12927  4sqlem15  12928  4sqlem17  12930  4sqlem19  12932  ennnfonelemkh  12983  ennnfonelemhf1o  12984  setscomd  13073  ressressg  13108  qusex  13358  qusin  13359  grpinvalem  13418  grpinva  13419  grprida  13420  gsumsplit1r  13431  isnsgrp  13439  sgrpass  13441  sgrp1  13444  sgrppropd  13446  prdssgrpd  13448  mnd12g  13461  mndpropd  13473  prdsidlem  13480  prdsmndd  13481  imasmnd2  13485  mhmex  13495  mhmlin  13500  grprcan  13570  grpinvid1  13585  isgrpinv  13587  grplcan  13595  grpasscan1  13596  grplmulf1o  13607  grpinvadd  13611  grpinvsub  13615  grpsubsub4  13626  grppnpcan2  13627  grpnpncan  13628  dfgrp3mlem  13631  dfgrp3m  13632  grplactcnv  13635  prdsinvlem  13641  imasgrp2  13647  mhmlem  13651  mhmid  13652  mhmmnd  13653  mulgnnp1  13667  mulg2  13668  mulgnn0p1  13670  mulgsubcl  13673  mulgneg  13677  mulgaddcomlem  13682  mulgaddcom  13683  mulgz  13687  mulgnn0dir  13689  mulgdirlem  13690  mulgdir  13691  mulgneg2  13693  mulgnnass  13694  mulgnn0ass  13695  mulgass  13696  mulgassr  13697  mulgmodid  13698  mulgsubdir  13699  submmulg  13703  isnsg3  13744  nmzsubg  13747  ssnmz  13748  0nsg  13751  eqger  13761  eqgid  13763  eqgcpbl  13765  ghmlin  13785  ghmmulg  13793  ghmnsgima  13805  ghmnsgpreima  13806  conjghm  13813  conjnmz  13816  ablsub2inv  13848  abladdsub4  13851  abladdsub  13852  ablpncan2  13853  ablpnpcan  13857  ablnncan  13858  ablnnncan1  13861  gsumfzconst  13878  gsumfzsnfd  13882  mgpress  13894  rngass  13902  rngdi  13903  rngdir  13904  rnglz  13908  rngmneg1  13910  rngsubdir  13915  rngpropd  13918  imasrng  13919  srgass  13934  srgmulgass  13952  srgpcomp  13953  srgpcompp  13954  srgpcomppsc  13955  ringpropd  14001  ringlz  14006  ring1eq0  14011  ringnegl  14014  ringmneg1  14016  ringsubdir  14020  mulgass2  14021  ring1  14022  imasring  14027  opprrng  14040  opprring  14042  unitgrp  14080  dvrcan1  14104  rdivmuldivd  14108  subrginv  14201  resrhm  14212  unitrrg  14231  islmod  14255  lmodlema  14256  islmodd  14257  lmod0vs  14285  lmodvs0  14286  lmodvsmmulgdi  14287  lmodvneg1  14294  lmodvsneg  14295  lmodsubvs  14307  lmodsubdi  14308  lmodsubdir  14309  lmodprop2d  14312  rmodislmodlem  14314  rmodislmod  14315  lsssetm  14320  islssmd  14323  lssclg  14328  lssvacl  14329  lss1d  14347  lsspropdg  14395  sraval  14401  rnglidlmcl  14444  gsumfzfsumlemm  14551  znunit  14623  mplsubgfilemcl  14663  resttop  14844  restco  14848  restin  14850  lmfval  14867  cnprcl2k  14880  txrest  14950  txdis1cn  14952  cnmpt2res  14971  psmettri2  15002  psmettri  15004  xmettri2  15035  xmettri  15046  mettri  15047  metrtri  15051  blvalps  15062  blval  15063  xblss2  15079  blhalf  15082  comet  15173  xmetxp  15181  txmetcnp  15192  cnmet  15204  ioo2bl  15225  ivthreinc  15319  limcmpted  15337  limcimolemlt  15338  cnplimclemr  15343  limccnp2cntop  15351  reldvg  15353  dvfvalap  15355  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvconst  15368  dvconstre  15370  dvconstss  15372  dvcnp2cntop  15373  dvaddxxbr  15375  dvmulxxbr  15376  dvcoapbr  15381  dvcjbr  15382  dvexp  15385  dvrecap  15387  dvmptcmulcn  15395  dveflem  15400  plyval  15406  elply2  15409  elplyr  15414  elplyd  15415  ply1termlem  15416  plyaddlem1  15421  plymullem1  15422  plycoeid3  15431  plycjlemc  15434  dvply1  15439  sin0pilem1  15455  sinperlem  15482  ptolemy  15498  tangtx  15512  abssinper  15520  reexplog  15545  relogexp  15546  cxprec  15584  rpdivcxp  15585  cxpmul  15586  rpabscxpbnd  15614  rplogbval  15619  rplogbreexp  15627  rprelogbmul  15629  logbrec  15634  logbgcd1irraplemap  15643  binom4  15653  wilthlem1  15654  mpodvdsmulf1o  15664  sgmppw  15666  0sgmppw  15667  1sgmprm  15668  1sgm2ppw  15669  perfectlem1  15673  perfectlem2  15674  perfect  15675  lgslem1  15679  lgslem4  15682  lgsval  15683  lgsfvalg  15684  lgsval2lem  15689  lgsval4lem  15690  lgsvalmod  15698  lgsneg  15703  lgsneg1  15704  lgsmod  15705  lgsdilem  15706  lgsdir2lem4  15710  lgsdir2  15712  lgsdirprm  15713  lgsdir  15714  lgsne0  15717  lgssq  15719  lgssq2  15720  lgsmulsqcoprm  15725  lgsdirnn0  15726  lgsdinn0  15727  gausslemma2dlem1a  15737  gausslemma2dlem4  15743  gausslemma2dlem5a  15744  gausslemma2dlem5  15745  gausslemma2dlem6  15746  gausslemma2dlem7  15747  gausslemma2d  15748  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisenlem4  15752  lgseisen  15753  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem1  15760  lgsquad2lem2  15761  lgsquad3  15763  m1lgs  15764  2lgslem1a  15767  2lgslem1c  15769  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2lgslem3a1  15776  2lgslem3b1  15777  2lgslem3c1  15778  2lgslem3d1  15779  2lgsoddprmlem1  15784  2lgsoddprmlem2  15785  2lgsoddprmlem3  15790  2sqlem1  15793  2sqlem2  15794  mul2sq  15795  2sqlem3  15796  2sqlem4  15797  2sqlem8  15802  2sqlem9  15803  2sqlem10  15804  uspgr2wlkeqi  16078  trilpolemeq1  16408  trilpolemlt1  16409  trirec0xor  16413  apdifflemf  16414  apdiff  16416