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  6750  nnmsucr  6766  nnm1  6803  nnm2  6804  ecovass  6923  ecoviass  6924  ecovdi  6925  ecovidi  6926  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  9689  zneo  9757  nneoor  9758  nneo  9759  zeo  9761  zeo2  9762  deceq1  9791  qreccl  10057  xaddcom  10279  xnegdi  10286  xaddass  10287  xaddass2  10288  xpncan  10289  xleadd1a  10291  xltadd1  10294  xposdif  10300  xadd4d  10303  lincmb01cmp  10421  lincmble  10422  iccf1o  10423  fzspl  10492  fz0to4untppr  10547  fzo0addel  10622  fzosubel3  10630  qavgle  10709  2tnp1ge0ge0  10756  fldiv4p1lem1div2  10760  fldiv4lem1div2  10762  ceilqm1lt  10769  flqdiv  10778  modqlt  10790  modqdiffl  10792  modqcyc2  10817  modqaddabs  10819  mulqaddmodid  10821  mulp1mod1  10822  modqmuladd  10823  modqmuladdnn0  10825  qnegmod  10826  addmodid  10829  addmodidr  10830  modqadd2mod  10831  modqm1p1mod0  10832  modqmul12d  10835  modqnegd  10836  modqadd12d  10837  modqsub12d  10838  q2submod  10842  modqmulmodr  10847  modqaddmulmod  10848  modqsubdir  10850  modfzo0difsn  10852  modsumfzodifsn  10853  addmodlteq  10855  frecuzrdgsuc  10871  frecfzennn  10883  iseqovex  10915  seq3-1p  10947  seq3caopr2  10950  seqcaopr2g  10951  seq3caopr  10952  seqcaoprg  10953  seqf1oglem2a  10975  seqf1oglem1  10976  seqf1oglem2  10977  seq3id  10982  seq3homo  10984  seq3z  10985  seqhomog  10987  seqfeq4g  10988  expp1  11003  exprecap  11037  expaddzaplem  11039  expmulzap  11042  expdivap  11047  sqval  11054  sqsubswap  11056  sqdividap  11061  subsq  11103  subsq2  11104  binom2  11108  binom2sub  11110  mulbinom2  11113  binom3  11114  zesq  11116  bernneq2  11119  modqexp  11124  sqoddm1div8  11151  mulsubdivbinom2ap  11170  nn0opthlem1d  11179  nn0opthd  11181  nn0opth2d  11182  facp1  11189  facdiv  11197  facndiv  11198  faclbnd  11200  faclbnd2  11201  faclbnd3  11202  bcval  11208  bccmpl  11213  bcm1k  11219  bcp1n  11220  bcp1nk  11221  bcval5  11222  bcp1m1  11224  bcpasc  11225  bcm1n  11228  bcn2m1  11229  hashprg  11270  hashdifpr  11282  hashfzo  11284  hashfzp1  11286  hashfz0  11287  hashxp  11288  hashfibclem  11303  hashfibc  11304  hashf1  11308  zfz1isolemsplit  11311  zfz1isolem1  11313  seq3coll  11315  lswwrd  11372  ccatfvalfi  11381  ccatass  11397  lswccatn0lsw  11400  wrdlenccats1lenm1g  11425  ccatw2s1leng  11427  ccatswrd  11463  ccatpfx  11494  swrdpfx  11500  pfxpfx  11501  ccats1pfxeq  11507  wrdeqs1cat  11513  wrdind  11515  wrd2ind  11516  pfxccatpfx2  11530  pfxccatin12d  11538  cats1catd  11561  cats2catd  11562  s2leng  11582  s3s4d  11596  s2s5d  11597  s5s2d  11598  reval  11635  crre  11643  remim  11646  remul2  11659  immul2  11666  imval2  11680  sq01  11681  cjdivap  11696  caucvgre  11768  cvg1nlemcau  11771  cvg1nlemres  11772  resqrexlemp1rp  11793  resqrexlemfp1  11796  resqrexlemover  11797  resqrexlemcalc1  11801  resqrexlemcalc3  11803  resqrexlemnm  11805  resqrexlemoverl  11808  resqrexlemglsq  11809  resqrexlemga  11810  resqrexlemsqa  11811  resqrexlemex  11812  resqrex  11813  sqrtdiv  11829  absvalsq  11840  absreimsq  11854  absdivap  11857  cau3lem  11902  maxabslemlub  11995  maxabslemval  11996  max0addsup  12007  minabs  12025  bdtrilem  12029  bdtri  12030  xrmaxaddlem  12050  xrmaxadd  12051  xrbdtri  12066  clim  12071  clim2  12073  climshftlemg  12092  climshft2  12096  climcn1  12098  climcn2  12099  subcn2  12101  reccn2ap  12103  climmulc2  12121  climsubc2  12123  clim2ser  12127  iser3shft  12136  climcau  12137  serf0  12142  fzosump1  12208  fsum1p  12209  fsump1  12211  sumsplitdc  12223  fsump1i  12224  mptfzshft  12233  fisum0diag2  12238  fsumconst  12245  fsumdifsnconst  12246  modfsummodlemstep  12248  modfsummod  12249  telfsumo  12257  fsumparts  12261  fsumrelem  12262  hash2iun1dif1  12271  binomlem  12274  binom  12275  binom1p  12276  binom1dif  12278  bcxmas  12280  isumsplit  12282  isum1p  12283  arisum  12289  arisum2  12290  trireciplem  12291  geoserap  12298  geolim  12302  geolim2  12303  georeclim  12304  geo2sum  12305  geoisum1  12310  cvgratnnlemseq  12317  cvgratnnlemsumlt  12319  cvgratnnlemfm  12320  cvgratz  12323  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  fprod1p  12390  fprodp1  12391  fprodcl2lem  12396  fprodfac  12406  fprodeq0  12408  fprodconst  12411  fprodrec  12420  fprodsplit1f  12425  fprodmodd  12432  efcllemp  12449  ef0lem  12451  efval  12452  esum  12453  ege2le3  12462  efaddlem  12465  efsep  12482  effsumlt  12483  eft0val  12484  efgt1p2  12486  efgt1p  12487  sinval  12493  cosval  12494  resinval  12506  recosval  12507  efi4p  12508  resin4p  12509  recos4p  12510  sinneg  12517  cosneg  12518  efival  12523  sinadd  12527  cosadd  12528  tanaddap  12530  sinmul  12535  cosmul  12536  cos2t  12541  cos2tsin  12542  ef01bndlem  12547  absefib  12562  demoivre  12564  demoivreALT  12565  eirraplem  12568  p1modz1  12585  dvdsmodexp  12586  moddvds  12590  mulmoddvds  12654  3dvds2dec  12657  zeo3  12659  odd2np1lem  12663  odd2np1  12664  oexpneg  12668  2tp1odd  12675  ltoddhalfle  12684  opoe  12686  opeo  12688  omeo  12689  m1expo  12691  m1exp1  12692  nn0o1gt2  12696  nn0o  12698  divalglemnn  12709  divalglemqt  12710  divalglemeunn  12712  divalglemex  12713  divalglemeuneg  12714  flodddiv4  12727  flodddiv4t2lthalf  12730  bitsp1o  12744  bitsmod  12747  bitsinv1lem  12752  gcdaddm  12785  bezoutlemnewy  12797  bezoutlema  12800  bezoutlemb  12801  bezoutlemex  12802  bezoutlemaz  12804  mulgcd  12817  gcddiv  12820  gcdmultiplez  12822  rpmulgcd  12827  rplpwr  12828  uzwodc  12838  lcmgcdlem  12879  lcmgcd  12880  divgcdcoprmex  12904  cncongr2  12906  prmexpb  12954  rpexp  12956  rpexp1i  12957  sqrt2irrlem  12964  nnmaxpwlemxy  12972  nnmaxpwlemndvds  12974  sqpweven  12979  2sqpwodd  12980  sqne2sq  12981  qmuldeneqnum  12999  nn0gcdsq  13004  zgcdsq  13005  numdensq  13006  dfphi2  13026  phiprmpw  13028  phiprm  13029  eulerthlema  13036  eulerthlemh  13037  eulerthlemth  13038  fermltl  13040  prmdiv  13041  prmdiveq  13042  prmdivdiv  13043  hashgcdlem  13044  odzval  13048  odzcllem  13049  odzdvds  13052  vfermltl  13058  powm2modprm  13059  reumodprminv  13060  modprm0  13061  nnnn0modprm0  13062  modprmn0modprm0  13063  coprimeprodsq  13064  coprimeprodsq2  13065  pythagtriplem1  13072  pythagtriplem3  13074  pythagtriplem4  13075  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem12  13082  pythagtriplem14  13084  pythagtriplem15  13085  pythagtriplem16  13086  pythagtriplem17  13087  pythagtriplem18  13088  pceu  13102  pczpre  13104  pcdiv  13109  pcqdiv  13114  pcrec  13115  pczndvds  13123  pcneg  13132  pc2dvds  13137  pcprmpw2  13140  pcaddlem  13146  pcadd  13147  fldivp1  13155  pockthlem  13163  pockthi  13165  4sqlem5  13189  4sqlem9  13193  4sqlem10  13194  4sqlem2  13196  4sqlem3  13197  4sqlem4  13199  mul4sqlem  13200  4sqlem11  13208  4sqlem12  13209  4sqlem14  13211  4sqlem15  13212  4sqlem17  13214  4sqlem19  13216  ballotfilem2  13285  ballotfilemfp1  13288  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilem4  13298  ballotfilemi1  13302  ballotfilemii  13303  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemsval  13309  ballotfilemsdom  13312  ballotfilemsima  13316  ballotfilemieq  13317  ballotfilemfrci  13328  ballotfilemth  13338  ballotfi  13339  ennnfonelemkh  13360  ennnfonelemhf1o  13361  setscomd  13450  ressressg  13487  qusex  13704  qusin  13705  grpinvalem  13763  grpinva  13764  grprida  13765  gzsumsplit1r  13773  isnsgrp  13779  sgrpass  13781  sgrp1  13784  sgrppropd  13786  mnd12g  13799  mndpropd  13811  imasmnd2  13817  mhmex  13827  mhmlin  13832  grprcan  13900  grpinvid1  13915  isgrpinv  13917  grplcan  13925  grpasscan1  13926  grplmulf1o  13937  grpinvadd  13941  grpinvsub  13945  grpsubsub4  13956  grppnpcan2  13957  grpnpncan  13958  dfgrp3mlem  13961  dfgrp3m  13962  grplactcnv  13965  imasgrp2  13971  mhmlem  13975  mhmid  13976  mhmmnd  13977  mulgnnp1  13991  mulg2  13992  mulgnn0p1  13994  mulgsubcl  13997  mulgneg  14001  mulgaddcomlem  14006  mulgaddcom  14007  mulgz  14011  mulgnn0dir  14013  mulgdirlem  14014  mulgdir  14015  mulgneg2  14017  mulgnnass  14018  mulgnn0ass  14019  mulgass  14020  mulgassr  14021  mulgmodid  14022  mulgsubdir  14023  submmulg  14027  isnsg3  14068  nmzsubg  14071  ssnmz  14072  0nsg  14075  eqger  14085  eqgid  14087  eqgcpbl  14089  ghmlin  14109  ghmmulg  14117  ghmnsgima  14129  ghmnsgpreima  14130  conjghm  14137  conjnmz  14140  cntzsgrpcl  14166  cntzsubm  14169  cntzsubg  14170  cntrsubgnsg  14174  ablsub2inv  14204  abladdsub4  14207  abladdsub  14208  ablpncan2  14209  ablpnpcan  14213  ablnncan  14214  ablnnncan1  14217  gzsumconst  14232  gzsumsnfd  14236  gzsumsplit0  14237  gzsumshift  14238  gzsumgsum  14244  gsummptfidmadd  14250  gsummptfidmsplit  14253  gsumresfi  14262  gsumconstcmn  14265  prdssgrpd  14297  prdsidlem  14299  prdsmndd  14300  prdsinvlem  14302  mgpress  14336  rngass  14344  rngdi  14345  rngdir  14346  rnglz  14350  rngmneg1  14352  rngsubdir  14357  rngpropd  14360  imasrng  14361  srgass  14381  srgmulgass  14399  srgpcomp  14400  srgpcompp  14401  srgpcomppsc  14402  ringpropd  14449  ringlz  14454  ring1eq0  14459  ringnegl  14462  ringmneg1  14464  ringsubdir  14468  mulgass2  14469  ring1  14470  imasring  14477  opprrng  14490  opprring  14492  unitgrp  14531  dvrcan1  14555  rdivmuldivd  14559  subrginv  14653  resrhm  14664  unitrrg  14684  aprlring  14708  islmod  14735  lmodlema  14736  islmodd  14737  lmod0vs  14766  lmodvs0  14767  lmodvsmmulgdi  14768  lmodvneg1  14775  lmodvsneg  14776  lmodsubvs  14788  lmodsubdi  14789  lmodsubdir  14790  lmodprop2d  14793  rmodislmodlem  14795  rmodislmod  14796  lsssetm  14801  islssmd  14804  lssclg  14809  lssvacl  14810  lss1d  14828  lsspropdg  14876  sraval  14882  rnglidlmcl  14925  znunit  15102  isassa  15110  assalem  15111  assa2ass  15117  assapropd  15122  asclmul1  15137  assamulgscmlem2  15150  psrlidmfi  15208  psrass1fi  15210  psrdirfi  15212  resttop  15413  restco  15417  restin  15419  lmfval  15436  cnprcl2k  15449  txrest  15519  txdis1cn  15521  cnmpt2res  15540  psmettri2  15571  psmettri  15573  xmettri2  15604  xmettri  15615  mettri  15616  metrtri  15620  blvalps  15631  blval  15632  xblss2  15648  blhalf  15651  comet  15742  xmetxp  15750  txmetcnp  15761  cnmet  15773  ioo2bl  15794  ivthreinc  15888  limcmpted  15906  limcimolemlt  15907  cnplimclemr  15912  limccnp2cntop  15920  reldvg  15922  dvfvalap  15924  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvconst  15937  dvconstre  15939  dvconstss  15941  dvcnp2cntop  15942  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  dvexp  15954  dvrecap  15956  dvmptcmulcn  15964  dveflem  15969  plyval  15975  elply2  15978  elplyr  15983  elplyd  15984  ply1termlem  15985  plyaddlem1  15990  plymullem1  15991  plycoeid3  16000  plycjlemc  16003  dvply1  16008  sin0pilem1  16025  sinperlem  16052  ptolemy  16068  tangtx  16082  abssinper  16090  reexplog  16118  relogexp  16119  cxprec  16160  rpdivcxp  16161  cxpmul  16162  rpabscxpbnd  16192  efnthr  16193  rplogbval  16198  rplogbreexp  16206  rprelogbmul  16208  logbrec  16213  logbgcd1irraplemap  16222  zprmlogbaplem1  16232  zprmlogbaplem3  16234  zprmlogbap  16235  binom4  16236  log2tlbndlog2  16237  log2ublem2  16239  birthdaylem2  16243  birthdaylem3  16244  pellexlem2  16247  pellexlem3  16248  wilthlem1  16249  ppiprm  16276  ppiqp1le  16284  mpodvdsmulf1o  16301  sgmppw  16303  0sgmppw  16304  1sgmprm  16305  1sgm2ppw  16306  ppiqub  16310  chtqleppi  16311  chtublem  16312  chtqub  16313  perfectlem1  16316  perfectlem2  16317  perfect  16318  bcctr  16319  pcbcctr  16320  bcmono  16321  bcp1ctr  16323  bclbnd  16324  bposlem3  16330  bposlem6  16333  bposlem9  16336  lgslem1  16341  lgslem4  16344  lgsval  16345  lgsfvalg  16346  lgsval2lem  16351  lgsval4lem  16352  lgsvalmod  16360  lgsneg  16365  lgsneg1  16366  lgsmod  16367  lgsdilem  16368  lgsdir2lem4  16372  lgsdir2  16374  lgsdirprm  16375  lgsdir  16376  lgsne0  16379  lgssq  16381  lgssq2  16382  lgsmulsqcoprm  16387  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem1a  16399  gausslemma2dlem4  16405  gausslemma2dlem5a  16406  gausslemma2dlem5  16407  gausslemma2dlem6  16408  gausslemma2dlem7  16409  gausslemma2d  16410  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgseisen  16415  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem1  16422  lgsquad2lem2  16423  lgsquad3  16425  m1lgs  16426  2lgslem1a  16429  2lgslem1c  16431  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2lgslem3a1  16438  2lgslem3b1  16439  2lgslem3c1  16440  2lgslem3d1  16441  2lgsoddprmlem1  16446  2lgsoddprmlem2  16447  2lgsoddprmlem3  16452  2sqlem1  16455  2sqlem2  16456  mul2sq  16457  2sqlem3  16458  2sqlem4  16459  2sqlem8  16464  2sqlem9  16465  2sqlem10  16466  vdegp1bid  16778  uspgr2wlkeqi  16830  isclwwlk  16857  clwwlkccatlem  16863  clwwlknonex2  16902  repiecele0  17298  repiecege0  17299  repiecef  17300  trilpolemeq1  17313  trilpolemlt1  17314  trirec0xor  17318  apdifflemf  17319  apdiff  17321  qdiff  17322