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  7560  addasspig  7698  mulasspig  7700  mulpipq2  7739  distrnqg  7755  ltsonq  7766  ltanqg  7768  ltmnqg  7769  ltexnqq  7776  archnqq  7785  prarloclemarch2  7787  enq0sym  7800  addnq0mo  7815  mulnq0mo  7816  addnnnq0  7817  nqpnq0nq  7821  nq0m0r  7824  nq0a0  7825  nnanq0  7826  distrnq0  7827  addassnq0  7830  addpinq1  7832  prarloclemlo  7862  prarloclem3  7865  prarloclem5  7868  prarloclemcalc  7870  addnqprllem  7895  addnqprulem  7896  appdivnq  7931  recexprlem1ssl  8001  recexprlem1ssu  8002  ltmprr  8010  cauappcvgprlemladdru  8024  cauappcvgprlem1  8027  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem1  8047  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemexb  8075  caucvgprprlem1  8077  addcmpblnr  8107  mulcmpblnrlemg  8108  addsrmo  8111  mulsrmo  8112  addsrpr  8113  mulsrpr  8114  ltsrprg  8115  1idsr  8136  pn0sr  8139  recexgt0sr  8141  mulgt0sr  8146  srpospr  8151  prsradd  8154  caucvgsrlemfv  8159  caucvgsrlemcau  8161  caucvgsrlemgt1  8163  caucvgsrlemoffval  8164  caucvgsrlemoffcau  8166  caucvgsrlemoffres  8168  caucvgsrlembnd  8169  caucvgsr  8170  map2psrprg  8173  pitonnlem1p1  8214  pitonnlem2  8215  pitonn  8216  recidpirqlemcalc  8225  ax1rid  8245  axrnegex  8247  axcnre  8249  recriota  8258  nntopi  8262  axcaucvglemval  8265  axcaucvglemcau  8266  axcaucvglemres  8267  mul12  8457  mul4  8460  muladd11  8461  readdcan  8468  muladd11r  8484  add12  8486  cnegex  8506  addcan  8508  negeu  8519  pncan2  8535  addsubass  8538  addsub  8539  2addsub  8542  addsubeq4  8543  subid  8547  subid1  8548  npncan  8549  nppcan  8550  nnpcan  8551  nnncan1  8564  npncan3  8566  pnpcan  8567  pnncan  8569  ppncan  8570  addsub4  8571  negsub  8576  subneg  8577  subeqxfrd  8691  mvlraddd  8692  mvlladdd  8693  mvrraddd  8694  subaddeqd  8697  ine0  8723  mulneg1  8724  ltadd2  8749  apreap  8918  cru  8933  recexap  8984  mulcanapd  8992  div23ap  9024  div13ap  9026  divmulassap  9028  divmulasscomap  9029  divcanap4  9032  muldivdirap  9040  divsubdirap  9041  divmuldivap  9045  divdivdivap  9046  divcanap5  9047  divmul13ap  9048  divmuleqap  9050  divdiv32ap  9053  divcanap7  9054  dmdcanap  9055  divdivap1  9056  divdivap2  9057  divadddivap  9060  divsubdivap  9061  conjmulap  9062  divneg2ap  9069  subrecap  9172  mvllmulapd  9175  lt2mul2div  9212  nndivtr  9349  2halves  9539  halfaddsub  9544  subhalfhalf  9545  avgle1  9551  avgle2  9552  div4p1lem1div2  9564  un0addcl  9601  un0mulcl  9602  peano2z  9685  zneo  9752  nneoor  9753  nneo  9754  zeo  9756  zeo2  9757  deceq1  9786  qreccl  10052  xaddcom  10274  xnegdi  10281  xaddass  10282  xaddass2  10283  xpncan  10284  xleadd1a  10286  xltadd1  10289  xposdif  10295  xadd4d  10298  lincmb01cmp  10416  lincmble  10417  iccf1o  10418  fzspl  10487  fz0to4untppr  10542  fzo0addel  10617  fzosubel3  10625  qavgle  10704  2tnp1ge0ge0  10751  fldiv4p1lem1div2  10755  fldiv4lem1div2  10757  ceilqm1lt  10764  flqdiv  10773  modqlt  10785  modqdiffl  10787  modqcyc2  10812  modqaddabs  10814  mulqaddmodid  10816  mulp1mod1  10817  modqmuladd  10818  modqmuladdnn0  10820  qnegmod  10821  addmodid  10824  addmodidr  10825  modqadd2mod  10826  modqm1p1mod0  10827  modqmul12d  10830  modqnegd  10831  modqadd12d  10832  modqsub12d  10833  q2submod  10837  modqmulmodr  10842  modqaddmulmod  10843  modqsubdir  10845  modfzo0difsn  10847  modsumfzodifsn  10848  addmodlteq  10850  frecuzrdgsuc  10866  frecfzennn  10878  iseqovex  10910  seq3-1p  10942  seq3caopr2  10945  seqcaopr2g  10946  seq3caopr  10947  seqcaoprg  10948  seqf1oglem2a  10970  seqf1oglem1  10971  seqf1oglem2  10972  seq3id  10977  seq3homo  10979  seq3z  10980  seqhomog  10982  seqfeq4g  10983  expp1  10998  exprecap  11032  expaddzaplem  11034  expmulzap  11037  expdivap  11042  sqval  11049  sqsubswap  11051  sqdividap  11056  subsq  11098  subsq2  11099  binom2  11103  binom2sub  11105  mulbinom2  11108  binom3  11109  zesq  11111  bernneq2  11114  modqexp  11119  sqoddm1div8  11146  mulsubdivbinom2ap  11165  nn0opthlem1d  11174  nn0opthd  11176  nn0opth2d  11177  facp1  11184  facdiv  11192  facndiv  11193  faclbnd  11195  faclbnd2  11196  faclbnd3  11197  bcval  11203  bccmpl  11208  bcm1k  11214  bcp1n  11215  bcp1nk  11216  bcval5  11217  bcp1m1  11219  bcpasc  11220  bcm1n  11223  bcn2m1  11224  hashprg  11265  hashdifpr  11277  hashfzo  11279  hashfzp1  11281  hashfz0  11282  hashxp  11283  hashfibclem  11298  hashfibc  11299  hashf1  11303  zfz1isolemsplit  11306  zfz1isolem1  11308  seq3coll  11310  lswwrd  11367  ccatfvalfi  11376  ccatass  11392  lswccatn0lsw  11395  wrdlenccats1lenm1g  11420  ccatw2s1leng  11422  ccatswrd  11458  ccatpfx  11489  swrdpfx  11495  pfxpfx  11496  ccats1pfxeq  11502  wrdeqs1cat  11508  wrdind  11510  wrd2ind  11511  pfxccatpfx2  11525  pfxccatin12d  11533  cats1catd  11556  cats2catd  11557  s2leng  11577  s3s4d  11591  s2s5d  11592  s5s2d  11593  reval  11630  crre  11638  remim  11641  remul2  11654  immul2  11661  imval2  11675  sq01  11676  cjdivap  11691  caucvgre  11763  cvg1nlemcau  11766  cvg1nlemres  11767  resqrexlemp1rp  11788  resqrexlemfp1  11791  resqrexlemover  11792  resqrexlemcalc1  11796  resqrexlemcalc3  11798  resqrexlemnm  11800  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemga  11805  resqrexlemsqa  11806  resqrexlemex  11807  resqrex  11808  sqrtdiv  11824  absvalsq  11835  absreimsq  11849  absdivap  11852  cau3lem  11897  maxabslemlub  11990  maxabslemval  11991  max0addsup  12002  minabs  12020  bdtrilem  12024  bdtri  12025  xrmaxaddlem  12045  xrmaxadd  12046  xrbdtri  12061  clim  12066  clim2  12068  climshftlemg  12087  climshft2  12091  climcn1  12093  climcn2  12094  subcn2  12096  reccn2ap  12098  climmulc2  12116  climsubc2  12118  clim2ser  12122  iser3shft  12131  climcau  12132  serf0  12137  fzosump1  12203  fsum1p  12204  fsump1  12206  sumsplitdc  12218  fsump1i  12219  mptfzshft  12228  fisum0diag2  12233  fsumconst  12240  fsumdifsnconst  12241  modfsummodlemstep  12243  modfsummod  12244  telfsumo  12252  fsumparts  12256  fsumrelem  12257  hash2iun1dif1  12266  binomlem  12269  binom  12270  binom1p  12271  binom1dif  12273  bcxmas  12275  isumsplit  12277  isum1p  12278  arisum  12284  arisum2  12285  trireciplem  12286  geoserap  12293  geolim  12297  geolim2  12298  georeclim  12299  geo2sum  12300  geoisum1  12305  cvgratnnlemseq  12312  cvgratnnlemsumlt  12314  cvgratnnlemfm  12315  cvgratz  12318  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  fprod1p  12385  fprodp1  12386  fprodcl2lem  12391  fprodfac  12401  fprodeq0  12403  fprodconst  12406  fprodrec  12415  fprodsplit1f  12420  fprodmodd  12427  efcllemp  12444  ef0lem  12446  efval  12447  esum  12448  ege2le3  12457  efaddlem  12460  efsep  12477  effsumlt  12478  eft0val  12479  efgt1p2  12481  efgt1p  12482  sinval  12488  cosval  12489  resinval  12501  recosval  12502  efi4p  12503  resin4p  12504  recos4p  12505  sinneg  12512  cosneg  12513  efival  12518  sinadd  12522  cosadd  12523  tanaddap  12525  sinmul  12530  cosmul  12531  cos2t  12536  cos2tsin  12537  ef01bndlem  12542  absefib  12557  demoivre  12559  demoivreALT  12560  eirraplem  12563  p1modz1  12580  dvdsmodexp  12581  moddvds  12585  mulmoddvds  12649  3dvds2dec  12652  zeo3  12654  odd2np1lem  12658  odd2np1  12659  oexpneg  12663  2tp1odd  12670  ltoddhalfle  12679  opoe  12681  opeo  12683  omeo  12684  m1expo  12686  m1exp1  12687  nn0o1gt2  12691  nn0o  12693  divalglemnn  12704  divalglemqt  12705  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  flodddiv4  12722  flodddiv4t2lthalf  12725  bitsp1o  12739  bitsmod  12742  bitsinv1lem  12747  gcdaddm  12780  bezoutlemnewy  12792  bezoutlema  12795  bezoutlemb  12796  bezoutlemex  12797  bezoutlemaz  12799  mulgcd  12812  gcddiv  12815  gcdmultiplez  12817  rpmulgcd  12822  rplpwr  12823  uzwodc  12833  lcmgcdlem  12874  lcmgcd  12875  divgcdcoprmex  12899  cncongr2  12901  prmexpb  12949  rpexp  12951  rpexp1i  12952  sqrt2irrlem  12959  nnmaxpwlemxy  12967  nnmaxpwlemndvds  12969  sqpweven  12974  2sqpwodd  12975  sqne2sq  12976  qmuldeneqnum  12994  nn0gcdsq  12999  zgcdsq  13000  numdensq  13001  dfphi2  13021  phiprmpw  13023  phiprm  13024  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  fermltl  13035  prmdiv  13036  prmdiveq  13037  prmdivdiv  13038  hashgcdlem  13039  odzval  13043  odzcllem  13044  odzdvds  13047  vfermltl  13053  powm2modprm  13054  reumodprminv  13055  modprm0  13056  nnnn0modprm0  13057  modprmn0modprm0  13058  coprimeprodsq  13059  coprimeprodsq2  13060  pythagtriplem1  13067  pythagtriplem3  13069  pythagtriplem4  13070  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem15  13080  pythagtriplem16  13081  pythagtriplem17  13082  pythagtriplem18  13083  pceu  13097  pczpre  13099  pcdiv  13104  pcqdiv  13109  pcrec  13110  pczndvds  13118  pcneg  13127  pc2dvds  13132  pcprmpw2  13135  pcaddlem  13141  pcadd  13142  fldivp1  13150  pockthlem  13158  pockthi  13160  4sqlem5  13184  4sqlem9  13188  4sqlem10  13189  4sqlem2  13191  4sqlem3  13192  4sqlem4  13194  mul4sqlem  13195  4sqlem11  13203  4sqlem12  13204  4sqlem14  13206  4sqlem15  13207  4sqlem17  13209  4sqlem19  13211  ballotfilem2  13280  ballotfilemfp1  13283  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilem4  13293  ballotfilemi1  13297  ballotfilemii  13298  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemsval  13304  ballotfilemsdom  13307  ballotfilemsima  13311  ballotfilemieq  13312  ballotfilemfrci  13323  ballotfilemth  13333  ballotfi  13334  ennnfonelemkh  13355  ennnfonelemhf1o  13356  setscomd  13445  ressressg  13482  qusex  13699  qusin  13700  grpinvalem  13758  grpinva  13759  grprida  13760  gzsumsplit1r  13768  isnsgrp  13774  sgrpass  13776  sgrp1  13779  sgrppropd  13781  mnd12g  13794  mndpropd  13806  imasmnd2  13812  mhmex  13822  mhmlin  13827  grprcan  13895  grpinvid1  13910  isgrpinv  13912  grplcan  13920  grpasscan1  13921  grplmulf1o  13932  grpinvadd  13936  grpinvsub  13940  grpsubsub4  13951  grppnpcan2  13952  grpnpncan  13953  dfgrp3mlem  13956  dfgrp3m  13957  grplactcnv  13960  imasgrp2  13966  mhmlem  13970  mhmid  13971  mhmmnd  13972  mulgnnp1  13986  mulg2  13987  mulgnn0p1  13989  mulgsubcl  13992  mulgneg  13996  mulgaddcomlem  14001  mulgaddcom  14002  mulgz  14006  mulgnn0dir  14008  mulgdirlem  14009  mulgdir  14010  mulgneg2  14012  mulgnnass  14013  mulgnn0ass  14014  mulgass  14015  mulgassr  14016  mulgmodid  14017  mulgsubdir  14018  submmulg  14022  isnsg3  14063  nmzsubg  14066  ssnmz  14067  0nsg  14070  eqger  14080  eqgid  14082  eqgcpbl  14084  ghmlin  14104  ghmmulg  14112  ghmnsgima  14124  ghmnsgpreima  14125  conjghm  14132  conjnmz  14135  cntzsgrpcl  14161  cntzsubm  14164  cntzsubg  14165  cntrsubgnsg  14169  ablsub2inv  14199  abladdsub4  14202  abladdsub  14203  ablpncan2  14204  ablpnpcan  14208  ablnncan  14209  ablnnncan1  14212  gzsumconst  14227  gzsumsnfd  14231  gzsumsplit0  14232  gzsumshift  14233  gzsumgsum  14239  gsummptfidmadd  14245  gsummptfidmsplit  14248  gsumresfi  14254  gsumconstcmn  14257  prdssgrpd  14282  prdsidlem  14284  prdsmndd  14285  prdsinvlem  14287  mgpress  14321  rngass  14329  rngdi  14330  rngdir  14331  rnglz  14335  rngmneg1  14337  rngsubdir  14342  rngpropd  14345  imasrng  14346  srgass  14366  srgmulgass  14384  srgpcomp  14385  srgpcompp  14386  srgpcomppsc  14387  ringpropd  14434  ringlz  14439  ring1eq0  14444  ringnegl  14447  ringmneg1  14449  ringsubdir  14453  mulgass2  14454  ring1  14455  imasring  14460  opprrng  14473  opprring  14475  unitgrp  14514  dvrcan1  14538  rdivmuldivd  14542  subrginv  14636  resrhm  14647  unitrrg  14667  aprlring  14691  islmod  14718  lmodlema  14719  islmodd  14720  lmod0vs  14749  lmodvs0  14750  lmodvsmmulgdi  14751  lmodvneg1  14758  lmodvsneg  14759  lmodsubvs  14771  lmodsubdi  14772  lmodsubdir  14773  lmodprop2d  14776  rmodislmodlem  14778  rmodislmod  14779  lsssetm  14784  islssmd  14787  lssclg  14792  lssvacl  14793  lss1d  14811  lsspropdg  14859  sraval  14865  rnglidlmcl  14908  znunit  15085  isassa  15093  assalem  15094  assa2ass  15100  assapropd  15105  asclmul1  15120  assamulgscmlem2  15133  psrlidmfi  15178  mplsubgfilemcl  15189  resttop  15370  restco  15374  restin  15376  lmfval  15393  cnprcl2k  15406  txrest  15476  txdis1cn  15478  cnmpt2res  15497  psmettri2  15528  psmettri  15530  xmettri2  15561  xmettri  15572  mettri  15573  metrtri  15577  blvalps  15588  blval  15589  xblss2  15605  blhalf  15608  comet  15699  xmetxp  15707  txmetcnp  15718  cnmet  15730  ioo2bl  15751  ivthreinc  15845  limcmpted  15863  limcimolemlt  15864  cnplimclemr  15869  limccnp2cntop  15877  reldvg  15879  dvfvalap  15881  dvidlemap  15891  dvidrelem  15892  dvidsslem  15893  dvconst  15894  dvconstre  15896  dvconstss  15898  dvcnp2cntop  15899  dvaddxxbr  15901  dvmulxxbr  15902  dvcoapbr  15907  dvcjbr  15908  dvexp  15911  dvrecap  15913  dvmptcmulcn  15921  dveflem  15926  plyval  15932  elply2  15935  elplyr  15940  elplyd  15941  ply1termlem  15942  plyaddlem1  15947  plymullem1  15948  plycoeid3  15957  plycjlemc  15960  dvply1  15965  sin0pilem1  15982  sinperlem  16009  ptolemy  16025  tangtx  16039  abssinper  16047  reexplog  16075  relogexp  16076  cxprec  16117  rpdivcxp  16118  cxpmul  16119  rpabscxpbnd  16149  efnthr  16150  rplogbval  16155  rplogbreexp  16163  rprelogbmul  16165  logbrec  16170  logbgcd1irraplemap  16179  zprmlogbaplem1  16189  zprmlogbaplem3  16191  zprmlogbap  16192  binom4  16193  log2tlbndlog2  16194  log2ublem2  16196  birthdaylem2  16200  birthdaylem3  16201  pellexlem2  16204  pellexlem3  16205  wilthlem1  16206  ppiprm  16233  ppiqp1le  16241  mpodvdsmulf1o  16258  sgmppw  16260  0sgmppw  16261  1sgmprm  16262  1sgm2ppw  16263  ppiqub  16267  chtqleppi  16268  chtublem  16269  chtqub  16270  perfectlem1  16273  perfectlem2  16274  perfect  16275  bcctr  16276  pcbcctr  16277  bcmono  16278  bcp1ctr  16280  bclbnd  16281  bposlem3  16287  bposlem6  16290  bposlem9  16293  lgslem1  16298  lgslem4  16301  lgsval  16302  lgsfvalg  16303  lgsval2lem  16308  lgsval4lem  16309  lgsvalmod  16317  lgsneg  16322  lgsneg1  16323  lgsmod  16324  lgsdilem  16325  lgsdir2lem4  16329  lgsdir2  16331  lgsdirprm  16332  lgsdir  16333  lgsne0  16336  lgssq  16338  lgssq2  16339  lgsmulsqcoprm  16344  lgsdirnn0  16345  lgsdinn0  16346  gausslemma2dlem1a  16356  gausslemma2dlem4  16362  gausslemma2dlem5a  16363  gausslemma2dlem5  16364  gausslemma2dlem6  16365  gausslemma2dlem7  16366  gausslemma2d  16367  lgseisenlem1  16368  lgseisenlem2  16369  lgseisenlem3  16370  lgseisenlem4  16371  lgseisen  16372  lgsquadlem1  16375  lgsquadlem2  16376  lgsquad2lem1  16379  lgsquad2lem2  16380  lgsquad3  16382  m1lgs  16383  2lgslem1a  16386  2lgslem1c  16388  2lgslem3a  16391  2lgslem3b  16392  2lgslem3c  16393  2lgslem3d  16394  2lgslem3a1  16395  2lgslem3b1  16396  2lgslem3c1  16397  2lgslem3d1  16398  2lgsoddprmlem1  16403  2lgsoddprmlem2  16404  2lgsoddprmlem3  16409  2sqlem1  16412  2sqlem2  16413  mul2sq  16414  2sqlem3  16415  2sqlem4  16416  2sqlem8  16421  2sqlem9  16422  2sqlem10  16423  vdegp1bid  16735  uspgr2wlkeqi  16787  isclwwlk  16814  clwwlkccatlem  16820  clwwlknonex2  16859  repiecele0  17254  repiecege0  17255  repiecef  17256  trilpolemeq1  17269  trilpolemlt1  17270  trirec0xor  17274  apdifflemf  17275  apdiff  17277  qdiff  17278