Theorem oveq1d 6103

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 6095	. 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 6088

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 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  fvoveq1d  6110  csbov2g  6130  caovassg  6251  caovdig  6267  caovdirg  6270  caov12d  6274  caov31d  6275  caov411d  6278  ofovex  6311  caofinvl  6332  suppofss1dcl  6508  suppofss2dcl  6509  omsuc  6749  nnmsucr  6765  nnm1  6802  nnm2  6803  ecovass  6922  ecoviass  6923  ecovdi  6924  ecovidi  6925  isacnm  7565  addasspig  7703  mulasspig  7705  mulpipq2  7744  distrnqg  7760  ltsonq  7771  ltanqg  7773  ltmnqg  7774  ltexnqq  7781  archnqq  7790  prarloclemarch2  7792  enq0sym  7805  addnq0mo  7820  mulnq0mo  7821  addnnnq0  7822  nqpnq0nq  7826  nq0m0r  7829  nq0a0  7830  nnanq0  7831  distrnq0  7832  addassnq0  7835  addpinq1  7837  prarloclemlo  7867  prarloclem3  7870  prarloclem5  7873  prarloclemcalc  7875  addnqprllem  7900  addnqprulem  7901  appdivnq  7936  recexprlem1ssl  8006  recexprlem1ssu  8007  ltmprr  8015  cauappcvgprlemladdru  8029  cauappcvgprlem1  8032  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemcl  8049  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem1  8052  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemexb  8080  caucvgprprlem1  8082  addcmpblnr  8112  mulcmpblnrlemg  8113  addsrmo  8116  mulsrmo  8117  addsrpr  8118  mulsrpr  8119  ltsrprg  8120  1idsr  8141  pn0sr  8144  recexgt0sr  8146  mulgt0sr  8151  srpospr  8156  prsradd  8159  caucvgsrlemfv  8164  caucvgsrlemcau  8166  caucvgsrlemgt1  8168  caucvgsrlemoffval  8169  caucvgsrlemoffcau  8171  caucvgsrlemoffres  8173  caucvgsrlembnd  8174  caucvgsr  8175  map2psrprg  8178  pitonnlem1p1  8219  pitonnlem2  8220  pitonn  8221  recidpirqlemcalc  8230  ax1rid  8250  axrnegex  8252  axcnre  8254  recriota  8263  nntopi  8267  axcaucvglemval  8270  axcaucvglemcau  8271  axcaucvglemres  8272  mul12  8462  mul4  8465  muladd11  8466  readdcan  8473  muladd11r  8489  add12  8491  cnegex  8511  addcan  8513  negeu  8524  pncan2  8540  addsubass  8543  addsub  8544  2addsub  8547  addsubeq4  8548  subid  8552  subid1  8553  npncan  8554  nppcan  8555  nnpcan  8556  nnncan1  8569  npncan3  8571  pnpcan  8572  pnncan  8574  ppncan  8575  addsub4  8576  negsub  8581  subneg  8582  subeqxfrd  8696  mvlraddd  8697  mvlladdd  8698  mvrraddd  8699  subaddeqd  8702  ine0  8728  mulneg1  8729  ltadd2  8754  apreap  8923  cru  8938  recexap  8989  mulcanapd  8997  div23ap  9029  div13ap  9031  divmulassap  9033  divmulasscomap  9034  divcanap4  9037  muldivdirap  9045  divsubdirap  9046  divmuldivap  9050  divdivdivap  9051  divcanap5  9052  divmul13ap  9053  divmuleqap  9055  divdiv32ap  9058  divcanap7  9059  dmdcanap  9060  divdivap1  9061  divdivap2  9062  divadddivap  9065  divsubdivap  9066  conjmulap  9067  divneg2ap  9074  subrecap  9177  mvllmulapd  9180  lt2mul2div  9217  nndivtr  9355  2halves  9545  halfaddsub  9550  subhalfhalf  9551  avgle1  9557  avgle2  9558  div4p1lem1div2  9570  un0addcl  9607  un0mulcl  9608  peano2z  9691  zneo  9758  nneoor  9759  nneo  9760  zeo  9762  zeo2  9763  deceq1  9792  qreccl  10058  xaddcom  10280  xnegdi  10287  xaddass  10288  xaddass2  10289  xpncan  10290  xleadd1a  10292  xltadd1  10295  xposdif  10301  xadd4d  10304  lincmb01cmp  10422  lincmble  10423  iccf1o  10424  fzspl  10493  fz0to4untppr  10548  fzo0addel  10623  fzosubel3  10631  qavgle  10710  2tnp1ge0ge0  10757  fldiv4p1lem1div2  10761  fldiv4lem1div2  10763  ceilqm1lt  10770  flqdiv  10779  modqlt  10791  modqdiffl  10793  modqcyc2  10818  modqaddabs  10820  mulqaddmodid  10822  mulp1mod1  10823  modqmuladd  10824  modqmuladdnn0  10826  qnegmod  10827  addmodid  10830  addmodidr  10831  modqadd2mod  10832  modqm1p1mod0  10833  modqmul12d  10836  modqnegd  10837  modqadd12d  10838  modqsub12d  10839  q2submod  10843  modqmulmodr  10848  modqaddmulmod  10849  modqsubdir  10851  modfzo0difsn  10853  modsumfzodifsn  10854  addmodlteq  10856  frecuzrdgsuc  10872  frecfzennn  10884  iseqovex  10916  seq3-1p  10948  seq3caopr2  10951  seqcaopr2g  10952  seq3caopr  10953  seqcaoprg  10954  seqf1oglem2a  10976  seqf1oglem1  10977  seqf1oglem2  10978  seq3id  10983  seq3homo  10985  seq3z  10986  seqhomog  10988  seqfeq4g  10989  expp1  11004  exprecap  11038  expaddzaplem  11040  expmulzap  11043  expdivap  11048  sqval  11055  sqsubswap  11057  sqdividap  11062  subsq  11104  subsq2  11105  binom2  11109  binom2sub  11111  mulbinom2  11114  binom3  11115  zesq  11117  bernneq2  11120  modqexp  11125  sqoddm1div8  11152  mulsubdivbinom2ap  11171  nn0opthlem1d  11180  nn0opthd  11182  nn0opth2d  11183  facp1  11190  facdiv  11198  facndiv  11199  faclbnd  11201  faclbnd2  11202  faclbnd3  11203  bcval  11209  bccmpl  11214  bcm1k  11220  bcp1n  11221  bcp1nk  11222  bcval5  11223  bcp1m1  11225  bcpasc  11226  bcm1n  11229  bcn2m1  11230  hashprg  11271  hashdifpr  11283  hashfzo  11285  hashfzp1  11287  hashfz0  11288  hashxp  11289  hashfibclem  11304  hashfibc  11305  hashf1  11309  zfz1isolemsplit  11312  zfz1isolem1  11314  seq3coll  11316  lswwrd  11373  ccatfvalfi  11382  ccatass  11398  lswccatn0lsw  11401  wrdlenccats1lenm1g  11426  ccatw2s1leng  11428  ccatswrd  11464  ccatpfx  11495  swrdpfx  11501  pfxpfx  11502  ccats1pfxeq  11508  wrdeqs1cat  11514  wrdind  11516  wrd2ind  11517  pfxccatpfx2  11531  pfxccatin12d  11539  cats1catd  11562  cats2catd  11563  s2leng  11583  s3s4d  11597  s2s5d  11598  s5s2d  11599  reval  11636  crre  11644  remim  11647  remul2  11660  immul2  11667  imval2  11681  sq01  11682  cjdivap  11697  caucvgre  11769  cvg1nlemcau  11772  cvg1nlemres  11773  resqrexlemp1rp  11794  resqrexlemfp1  11797  resqrexlemover  11798  resqrexlemcalc1  11802  resqrexlemcalc3  11804  resqrexlemnm  11806  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemga  11811  resqrexlemsqa  11812  resqrexlemex  11813  resqrex  11814  sqrtdiv  11830  absvalsq  11841  absreimsq  11855  absdivap  11858  cau3lem  11903  maxabslemlub  11996  maxabslemval  11997  max0addsup  12008  minabs  12026  bdtrilem  12030  bdtri  12031  xrmaxaddlem  12051  xrmaxadd  12052  xrbdtri  12067  clim  12072  clim2  12074  climshftlemg  12093  climshft2  12097  climcn1  12099  climcn2  12100  subcn2  12102  reccn2ap  12104  climmulc2  12122  climsubc2  12124  clim2ser  12128  iser3shft  12137  climcau  12138  serf0  12143  fzosump1  12209  fsum1p  12210  fsump1  12212  sumsplitdc  12224  fsump1i  12225  mptfzshft  12234  fisum0diag2  12239  fsumconst  12246  fsumdifsnconst  12247  modfsummodlemstep  12249  modfsummod  12250  telfsumo  12258  fsumparts  12262  fsumrelem  12263  hash2iun1dif1  12272  binomlem  12275  binom  12276  binom1p  12277  binom1dif  12279  bcxmas  12281  isumsplit  12283  isum1p  12284  arisum  12290  arisum2  12291  trireciplem  12292  geoserap  12299  geolim  12303  geolim2  12304  georeclim  12305  geo2sum  12306  geoisum1  12311  cvgratnnlemseq  12318  cvgratnnlemsumlt  12320  cvgratnnlemfm  12321  cvgratz  12324  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  fprod1p  12391  fprodp1  12392  fprodcl2lem  12397  fprodfac  12407  fprodeq0  12409  fprodconst  12412  fprodrec  12421  fprodsplit1f  12426  fprodmodd  12433  efcllemp  12450  ef0lem  12452  efval  12453  esum  12454  ege2le3  12463  efaddlem  12466  efsep  12483  effsumlt  12484  eft0val  12485  efgt1p2  12487  efgt1p  12488  sinval  12494  cosval  12495  resinval  12507  recosval  12508  efi4p  12509  resin4p  12510  recos4p  12511  sinneg  12518  cosneg  12519  efival  12524  sinadd  12528  cosadd  12529  tanaddap  12531  sinmul  12536  cosmul  12537  cos2t  12542  cos2tsin  12543  ef01bndlem  12548  absefib  12563  demoivre  12565  demoivreALT  12566  eirraplem  12569  p1modz1  12586  dvdsmodexp  12587  moddvds  12591  mulmoddvds  12655  3dvds2dec  12658  zeo3  12660  odd2np1lem  12664  odd2np1  12665  oexpneg  12669  2tp1odd  12676  ltoddhalfle  12685  opoe  12687  opeo  12689  omeo  12690  m1expo  12692  m1exp1  12693  nn0o1gt2  12697  nn0o  12699  divalglemnn  12710  divalglemqt  12711  divalglemeunn  12713  divalglemex  12714  divalglemeuneg  12715  flodddiv4  12728  flodddiv4t2lthalf  12731  bitsp1o  12745  bitsmod  12748  bitsinv1lem  12753  gcdaddm  12786  bezoutlemnewy  12798  bezoutlema  12801  bezoutlemb  12802  bezoutlemex  12803  bezoutlemaz  12805  mulgcd  12818  gcddiv  12821  gcdmultiplez  12823  rpmulgcd  12828  rplpwr  12829  uzwodc  12839  lcmgcdlem  12880  lcmgcd  12881  divgcdcoprmex  12905  cncongr2  12907  prmexpb  12955  rpexp  12957  rpexp1i  12958  sqrt2irrlem  12965  nnmaxpwlemxy  12973  nnmaxpwlemndvds  12975  sqpweven  12980  2sqpwodd  12981  sqne2sq  12982  qmuldeneqnum  13000  nn0gcdsq  13005  zgcdsq  13006  numdensq  13007  dfphi2  13027  phiprmpw  13029  phiprm  13030  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  fermltl  13041  prmdiv  13042  prmdiveq  13043  prmdivdiv  13044  hashgcdlem  13045  odzval  13049  odzcllem  13050  odzdvds  13053  vfermltl  13059  powm2modprm  13060  reumodprminv  13061  modprm0  13062  nnnn0modprm0  13063  modprmn0modprm0  13064  coprimeprodsq  13065  coprimeprodsq2  13066  pythagtriplem1  13073  pythagtriplem3  13075  pythagtriplem4  13076  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem15  13086  pythagtriplem16  13087  pythagtriplem17  13088  pythagtriplem18  13089  pceu  13103  pczpre  13105  pcdiv  13110  pcqdiv  13115  pcrec  13116  pczndvds  13124  pcneg  13133  pc2dvds  13138  pcprmpw2  13141  pcaddlem  13147  pcadd  13148  fldivp1  13156  pockthlem  13164  pockthi  13166  4sqlem5  13190  4sqlem9  13194  4sqlem10  13195  4sqlem2  13197  4sqlem3  13198  4sqlem4  13200  mul4sqlem  13201  4sqlem11  13209  4sqlem12  13210  4sqlem14  13212  4sqlem15  13213  4sqlem17  13215  4sqlem19  13217  ballotfilem2  13286  ballotfilemfp1  13289  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilem4  13299  ballotfilemi1  13303  ballotfilemii  13304  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemsval  13310  ballotfilemsdom  13313  ballotfilemsima  13317  ballotfilemieq  13318  ballotfilemfrci  13329  ballotfilemth  13339  ballotfi  13340  ennnfonelemkh  13361  ennnfonelemhf1o  13362  setscomd  13451  ressressg  13488  qusex  13705  qusin  13706  grpinvalem  13764  grpinva  13765  grprida  13766  gzsumsplit1r  13774  isnsgrp  13780  sgrpass  13782  sgrp1  13785  sgrppropd  13787  mnd12g  13800  mndpropd  13812  imasmnd2  13818  mhmex  13828  mhmlin  13833  grprcan  13901  grpinvid1  13916  isgrpinv  13918  grplcan  13926  grpasscan1  13927  grplmulf1o  13938  grpinvadd  13942  grpinvsub  13946  grpsubsub4  13957  grppnpcan2  13958  grpnpncan  13959  dfgrp3mlem  13962  dfgrp3m  13963  grplactcnv  13966  imasgrp2  13972  mhmlem  13976  mhmid  13977  mhmmnd  13978  mulgnnp1  13992  mulg2  13993  mulgnn0p1  13995  mulgsubcl  13998  mulgneg  14002  mulgaddcomlem  14007  mulgaddcom  14008  mulgz  14012  mulgnn0dir  14014  mulgdirlem  14015  mulgdir  14016  mulgneg2  14018  mulgnnass  14019  mulgnn0ass  14020  mulgass  14021  mulgassr  14022  mulgmodid  14023  mulgsubdir  14024  submmulg  14028  isnsg3  14069  nmzsubg  14072  ssnmz  14073  0nsg  14076  eqger  14086  eqgid  14088  eqgcpbl  14090  ghmlin  14110  ghmmulg  14118  ghmnsgima  14130  ghmnsgpreima  14131  conjghm  14138  conjnmz  14141  cntzsgrpcl  14167  cntzsubm  14170  cntzsubg  14171  cntrsubgnsg  14175  ablsub2inv  14205  abladdsub4  14208  abladdsub  14209  ablpncan2  14210  ablpnpcan  14214  ablnncan  14215  ablnnncan1  14218  gzsumconst  14233  gzsumsnfd  14237  gzsumsplit0  14238  gzsumshift  14239  gzsumgsum  14245  gsummptfidmadd  14251  gsummptfidmsplit  14254  gsumresfi  14263  gsumconstcmn  14266  prdssgrpd  14298  prdsidlem  14300  prdsmndd  14301  prdsinvlem  14303  mgpress  14337  rngass  14345  rngdi  14346  rngdir  14347  rnglz  14351  rngmneg1  14353  rngsubdir  14358  rngpropd  14361  imasrng  14362  srgass  14382  srgmulgass  14400  srgpcomp  14401  srgpcompp  14402  srgpcomppsc  14403  ringpropd  14450  ringlz  14455  ring1eq0  14460  ringnegl  14463  ringmneg1  14465  ringsubdir  14469  mulgass2  14470  ring1  14471  imasring  14478  opprrng  14491  opprring  14493  unitgrp  14532  dvrcan1  14556  rdivmuldivd  14560  subrginv  14654  resrhm  14665  unitrrg  14685  aprlring  14709  islmod  14736  lmodlema  14737  islmodd  14738  lmod0vs  14767  lmodvs0  14768  lmodvsmmulgdi  14769  lmodvneg1  14776  lmodvsneg  14777  lmodsubvs  14789  lmodsubdi  14790  lmodsubdir  14791  lmodprop2d  14794  rmodislmodlem  14796  rmodislmod  14797  lsssetm  14802  islssmd  14805  lssclg  14810  lssvacl  14811  lss1d  14829  lsspropdg  14877  sraval  14883  rnglidlmcl  14926  znunit  15103  isassa  15111  assalem  15112  assa2ass  15118  assapropd  15123  asclmul1  15138  assamulgscmlem2  15151  psrlidmfi  15199  psrass1fi  15201  psrdirfi  15203  mplsubgfilemcl  15215  resttop  15396  restco  15400  restin  15402  lmfval  15419  cnprcl2k  15432  txrest  15502  txdis1cn  15504  cnmpt2res  15523  psmettri2  15554  psmettri  15556  xmettri2  15587  xmettri  15598  mettri  15599  metrtri  15603  blvalps  15614  blval  15615  xblss2  15631  blhalf  15634  comet  15725  xmetxp  15733  txmetcnp  15744  cnmet  15756  ioo2bl  15777  ivthreinc  15871  limcmpted  15889  limcimolemlt  15890  cnplimclemr  15895  limccnp2cntop  15903  reldvg  15905  dvfvalap  15907  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvconst  15920  dvconstre  15922  dvconstss  15924  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvcjbr  15934  dvexp  15937  dvrecap  15939  dvmptcmulcn  15947  dveflem  15952  plyval  15958  elply2  15961  elplyr  15966  elplyd  15967  ply1termlem  15968  plyaddlem1  15973  plymullem1  15974  plycoeid3  15983  plycjlemc  15986  dvply1  15991  sin0pilem1  16008  sinperlem  16035  ptolemy  16051  tangtx  16065  abssinper  16073  reexplog  16101  relogexp  16102  cxprec  16143  rpdivcxp  16144  cxpmul  16145  rpabscxpbnd  16175  efnthr  16176  rplogbval  16181  rplogbreexp  16189  rprelogbmul  16191  logbrec  16196  logbgcd1irraplemap  16205  zprmlogbaplem1  16215  zprmlogbaplem3  16217  zprmlogbap  16218  binom4  16219  log2tlbndlog2  16220  log2ublem2  16222  birthdaylem2  16226  birthdaylem3  16227  pellexlem2  16230  pellexlem3  16231  wilthlem1  16232  ppiprm  16259  ppiqp1le  16267  mpodvdsmulf1o  16284  sgmppw  16286  0sgmppw  16287  1sgmprm  16288  1sgm2ppw  16289  ppiqub  16293  chtqleppi  16294  chtublem  16295  chtqub  16296  perfectlem1  16299  perfectlem2  16300  perfect  16301  bcctr  16302  pcbcctr  16303  bcmono  16304  bcp1ctr  16306  bclbnd  16307  bposlem3  16313  bposlem6  16316  bposlem9  16319  lgslem1  16324  lgslem4  16327  lgsval  16328  lgsfvalg  16329  lgsval2lem  16334  lgsval4lem  16335  lgsvalmod  16343  lgsneg  16348  lgsneg1  16349  lgsmod  16350  lgsdilem  16351  lgsdir2lem4  16355  lgsdir2  16357  lgsdirprm  16358  lgsdir  16359  lgsne0  16362  lgssq  16364  lgssq2  16365  lgsmulsqcoprm  16370  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem1a  16382  gausslemma2dlem4  16388  gausslemma2dlem5a  16389  gausslemma2dlem5  16390  gausslemma2dlem6  16391  gausslemma2dlem7  16392  gausslemma2d  16393  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  lgseisen  16398  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem1  16405  lgsquad2lem2  16406  lgsquad3  16408  m1lgs  16409  2lgslem1a  16412  2lgslem1c  16414  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgslem3a1  16421  2lgslem3b1  16422  2lgslem3c1  16423  2lgslem3d1  16424  2lgsoddprmlem1  16429  2lgsoddprmlem2  16430  2lgsoddprmlem3  16435  2sqlem1  16438  2sqlem2  16439  mul2sq  16440  2sqlem3  16441  2sqlem4  16442  2sqlem8  16447  2sqlem9  16448  2sqlem10  16449  vdegp1bid  16761  uspgr2wlkeqi  16813  isclwwlk  16840  clwwlkccatlem  16846  clwwlknonex2  16885  repiecele0  17281  repiecege0  17282  repiecef  17283  trilpolemeq1  17296  trilpolemlt1  17297  trirec0xor  17301  apdifflemf  17302  apdiff  17304  qdiff  17305