Theorem oveq1d 5889

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 5881	. 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 1353  (class class class)co 5874

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877

This theorem is referenced by:  fvoveq1d  5896  csbov2g  5915  caovassg  6032  caovdig  6048  caovdirg  6051  caov12d  6055  caov31d  6056  caov411d  6059  caofinvl  6104  omsuc  6472  nnmsucr  6488  nnm1  6525  nnm2  6526  ecovass  6643  ecoviass  6644  ecovdi  6645  ecovidi  6646  addasspig  7328  mulasspig  7330  mulpipq2  7369  distrnqg  7385  ltsonq  7396  ltanqg  7398  ltmnqg  7399  ltexnqq  7406  archnqq  7415  prarloclemarch2  7417  enq0sym  7430  addnq0mo  7445  mulnq0mo  7446  addnnnq0  7447  nqpnq0nq  7451  nq0m0r  7454  nq0a0  7455  nnanq0  7456  distrnq0  7457  addassnq0  7460  addpinq1  7462  prarloclemlo  7492  prarloclem3  7495  prarloclem5  7498  prarloclemcalc  7500  addnqprllem  7525  addnqprulem  7526  appdivnq  7561  recexprlem1ssl  7631  recexprlem1ssu  7632  ltmprr  7640  cauappcvgprlemladdru  7654  cauappcvgprlem1  7657  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprlem1  7677  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemexb  7705  caucvgprprlem1  7707  addcmpblnr  7737  mulcmpblnrlemg  7738  addsrmo  7741  mulsrmo  7742  addsrpr  7743  mulsrpr  7744  ltsrprg  7745  1idsr  7766  pn0sr  7769  recexgt0sr  7771  mulgt0sr  7776  srpospr  7781  prsradd  7784  caucvgsrlemfv  7789  caucvgsrlemcau  7791  caucvgsrlemgt1  7793  caucvgsrlemoffval  7794  caucvgsrlemoffcau  7796  caucvgsrlemoffres  7798  caucvgsrlembnd  7799  caucvgsr  7800  map2psrprg  7803  pitonnlem1p1  7844  pitonnlem2  7845  pitonn  7846  recidpirqlemcalc  7855  ax1rid  7875  axrnegex  7877  axcnre  7879  recriota  7888  nntopi  7892  axcaucvglemval  7895  axcaucvglemcau  7896  axcaucvglemres  7897  mul12  8085  mul4  8088  muladd11  8089  readdcan  8096  muladd11r  8112  add12  8114  cnegex  8134  addcan  8136  negeu  8147  pncan2  8163  addsubass  8166  addsub  8167  2addsub  8170  addsubeq4  8171  subid  8175  subid1  8176  npncan  8177  nppcan  8178  nnpcan  8179  nnncan1  8192  npncan3  8194  pnpcan  8195  pnncan  8197  ppncan  8198  addsub4  8199  negsub  8204  subneg  8205  subeqxfrd  8319  mvlraddd  8320  mvlladdd  8321  mvrraddd  8322  subaddeqd  8325  ine0  8350  mulneg1  8351  ltadd2  8375  apreap  8543  cru  8558  recexap  8609  mulcanapd  8617  div23ap  8647  div13ap  8649  divmulassap  8651  divmulasscomap  8652  divcanap4  8655  muldivdirap  8663  divsubdirap  8664  divmuldivap  8668  divdivdivap  8669  divcanap5  8670  divmul13ap  8671  divmuleqap  8673  divdiv32ap  8676  divcanap7  8677  dmdcanap  8678  divdivap1  8679  divdivap2  8680  divadddivap  8683  divsubdivap  8684  conjmulap  8685  divneg2ap  8692  subrecap  8795  mvllmulapd  8798  lt2mul2div  8835  nndivtr  8960  2halves  9147  halfaddsub  9152  avgle1  9158  avgle2  9159  div4p1lem1div2  9171  un0addcl  9208  un0mulcl  9209  peano2z  9288  zneo  9353  nneoor  9354  nneo  9355  zeo  9357  zeo2  9358  deceq1  9387  qreccl  9641  xaddcom  9860  xnegdi  9867  xaddass  9868  xaddass2  9869  xpncan  9870  xleadd1a  9872  xltadd1  9875  xposdif  9881  xadd4d  9884  lincmb01cmp  10002  iccf1o  10003  fz0to4untppr  10123  fzosubel3  10195  qavgle  10258  2tnp1ge0ge0  10300  fldiv4p1lem1div2  10304  ceilqm1lt  10311  flqdiv  10320  modqlt  10332  modqdiffl  10334  modqcyc2  10359  modqaddabs  10361  mulqaddmodid  10363  mulp1mod1  10364  modqmuladd  10365  modqmuladdnn0  10367  qnegmod  10368  addmodid  10371  addmodidr  10372  modqadd2mod  10373  modqm1p1mod0  10374  modqmul12d  10377  modqnegd  10378  modqadd12d  10379  modqsub12d  10380  q2submod  10384  modqmulmodr  10389  modqaddmulmod  10390  modqsubdir  10392  modfzo0difsn  10394  modsumfzodifsn  10395  addmodlteq  10397  frecuzrdgsuc  10413  frecfzennn  10425  iseqovex  10455  seq3-1p  10479  seq3caopr2  10481  seq3caopr  10482  seq3id  10507  seq3homo  10509  seq3z  10510  expp1  10526  exprecap  10560  expaddzaplem  10562  expmulzap  10565  expdivap  10570  sqval  10577  sqsubswap  10579  sqdividap  10584  subsq  10626  subsq2  10627  binom2  10631  binom2sub  10633  mulbinom2  10636  binom3  10637  zesq  10638  bernneq2  10641  modqexp  10646  sqoddm1div8  10673  mulsubdivbinom2ap  10690  nn0opthlem1d  10699  nn0opthd  10701  nn0opth2d  10702  facp1  10709  facdiv  10717  facndiv  10718  faclbnd  10720  faclbnd2  10721  faclbnd3  10722  bcval  10728  bccmpl  10733  bcm1k  10739  bcp1n  10740  bcp1nk  10741  bcval5  10742  bcp1m1  10744  bcpasc  10745  bcn2m1  10748  hashprg  10787  hashdifpr  10799  hashfzo  10801  hashfzp1  10803  hashfz0  10804  hashxp  10805  zfz1isolemsplit  10817  zfz1isolem1  10819  seq3coll  10821  reval  10857  crre  10865  remim  10868  remul2  10881  immul2  10888  imval2  10902  cjdivap  10917  caucvgre  10989  cvg1nlemcau  10992  cvg1nlemres  10993  resqrexlemp1rp  11014  resqrexlemfp1  11017  resqrexlemover  11018  resqrexlemcalc1  11022  resqrexlemcalc3  11024  resqrexlemnm  11026  resqrexlemoverl  11029  resqrexlemglsq  11030  resqrexlemga  11031  resqrexlemsqa  11032  resqrexlemex  11033  resqrex  11034  sqrtdiv  11050  absvalsq  11061  absreimsq  11075  absdivap  11078  cau3lem  11122  maxabslemlub  11215  maxabslemval  11216  max0addsup  11227  minabs  11243  bdtrilem  11246  bdtri  11247  xrmaxaddlem  11267  xrmaxadd  11268  xrbdtri  11283  clim  11288  clim2  11290  climshftlemg  11309  climshft2  11313  climcn1  11315  climcn2  11316  subcn2  11318  reccn2ap  11320  climmulc2  11338  climsubc2  11340  clim2ser  11344  iser3shft  11353  climcau  11354  serf0  11359  fzosump1  11424  fsum1p  11425  fsump1  11427  sumsplitdc  11439  fsump1i  11440  mptfzshft  11449  fisum0diag2  11454  fsumconst  11461  fsumdifsnconst  11462  modfsummodlemstep  11464  modfsummod  11465  telfsumo  11473  fsumparts  11477  fsumrelem  11478  hash2iun1dif1  11487  binomlem  11490  binom  11491  binom1p  11492  binom1dif  11494  bcxmas  11496  isumsplit  11498  isum1p  11499  arisum  11505  arisum2  11506  trireciplem  11507  geoserap  11514  geolim  11518  geolim2  11519  georeclim  11520  geo2sum  11521  geoisum1  11526  cvgratnnlemseq  11533  cvgratnnlemsumlt  11535  cvgratnnlemfm  11536  cvgratz  11539  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  fprod1p  11606  fprodp1  11607  fprodcl2lem  11612  fprodfac  11622  fprodeq0  11624  fprodconst  11627  fprodrec  11636  fprodsplit1f  11641  fprodmodd  11648  efcllemp  11665  ef0lem  11667  efval  11668  esum  11669  ege2le3  11678  efaddlem  11681  efsep  11698  effsumlt  11699  eft0val  11700  efgt1p2  11702  efgt1p  11703  sinval  11709  cosval  11710  resinval  11722  recosval  11723  efi4p  11724  resin4p  11725  recos4p  11726  sinneg  11733  cosneg  11734  efival  11739  sinadd  11743  cosadd  11744  tanaddap  11746  sinmul  11751  cosmul  11752  cos2t  11757  cos2tsin  11758  ef01bndlem  11763  absefib  11777  demoivre  11779  demoivreALT  11780  eirraplem  11783  p1modz1  11800  dvdsmodexp  11801  moddvds  11805  mulmoddvds  11868  3dvds2dec  11870  zeo3  11872  odd2np1lem  11876  odd2np1  11877  oexpneg  11881  2tp1odd  11888  ltoddhalfle  11897  opoe  11899  opeo  11901  omeo  11902  m1expo  11904  m1exp1  11905  nn0o1gt2  11909  nn0o  11911  divalglemnn  11922  divalglemqt  11923  divalglemeunn  11925  divalglemex  11926  divalglemeuneg  11927  flodddiv4  11938  flodddiv4t2lthalf  11941  gcdaddm  11984  bezoutlemnewy  11996  bezoutlema  11999  bezoutlemb  12000  bezoutlemex  12001  bezoutlemaz  12003  mulgcd  12016  gcddiv  12019  gcdmultiplez  12021  rpmulgcd  12026  rplpwr  12027  uzwodc  12037  lcmgcdlem  12076  lcmgcd  12077  divgcdcoprmex  12101  cncongr2  12103  prmexpb  12150  rpexp  12152  rpexp1i  12153  sqrt2irrlem  12160  oddpwdclemxy  12168  oddpwdclemndvds  12170  sqpweven  12174  2sqpwodd  12175  sqne2sq  12176  qmuldeneqnum  12194  nn0gcdsq  12199  zgcdsq  12200  numdensq  12201  dfphi2  12219  phiprmpw  12221  phiprm  12222  eulerthlema  12229  eulerthlemh  12230  eulerthlemth  12231  fermltl  12233  prmdiv  12234  prmdiveq  12235  prmdivdiv  12236  hashgcdlem  12237  odzval  12240  odzcllem  12241  odzdvds  12244  vfermltl  12250  powm2modprm  12251  reumodprminv  12252  modprm0  12253  nnnn0modprm0  12254  modprmn0modprm0  12255  coprimeprodsq  12256  coprimeprodsq2  12257  pythagtriplem1  12264  pythagtriplem3  12266  pythagtriplem4  12267  pythagtriplem6  12269  pythagtriplem7  12270  pythagtriplem12  12274  pythagtriplem14  12276  pythagtriplem15  12277  pythagtriplem16  12278  pythagtriplem17  12279  pythagtriplem18  12280  pceu  12294  pczpre  12296  pcdiv  12301  pcqdiv  12306  pcrec  12307  pczndvds  12314  pcneg  12323  pc2dvds  12328  pcprmpw2  12331  pcaddlem  12337  pcadd  12338  fldivp1  12345  pockthlem  12353  pockthi  12355  4sqlem5  12379  4sqlem9  12383  4sqlem10  12384  4sqlem2  12386  4sqlem3  12387  4sqlem4  12389  mul4sqlem  12390  ennnfonelemkh  12412  ennnfonelemhf1o  12413  setscomd  12502  ressressg  12533  qusin  12745  grprinvlem  12803  grprinvd  12804  grpridd  12805  isnsgrp  12811  sgrpass  12813  sgrp1  12815  mnd12g  12828  mndpropd  12840  mhmlin  12857  grprcan  12909  grpinvid1  12923  isgrpinv  12925  grplcan  12931  grpasscan1  12932  grplmulf1o  12943  grpinvadd  12947  grpinvsub  12951  grpsubsub4  12962  grppnpcan2  12963  grpnpncan  12964  dfgrp3mlem  12967  dfgrp3m  12968  grplactcnv  12971  mhmlem  12977  mhmid  12978  mhmmnd  12979  mulgnnp1  12990  mulg2  12991  mulgnn0p1  12993  mulgsubcl  12996  mulgneg  13000  mulgaddcomlem  13004  mulgaddcom  13005  mulgz  13009  mulgnn0dir  13011  mulgdirlem  13012  mulgdir  13013  mulgneg2  13015  mulgnnass  13016  mulgnn0ass  13017  mulgass  13018  mulgassr  13019  mulgmodid  13020  mulgsubdir  13021  isnsg3  13065  nmzsubg  13068  ssnmz  13069  0nsg  13072  eqger  13081  eqgid  13083  eqgcpbl  13085  ablsub2inv  13112  abladdsub4  13115  abladdsub  13116  ablpncan2  13117  ablpnpcan  13121  ablnncan  13122  ablnnncan1  13125  mgpress  13139  srgass  13152  srgmulgass  13170  srgpcomp  13171  srgpcompp  13172  srgpcomppsc  13173  ringpropd  13215  ringlz  13220  ring1eq0  13223  ringnegl  13226  ringmneg1  13228  rngsubdir  13232  mulgass2  13233  ring1  13234  opprring  13247  unitgrp  13283  dvrcan1  13307  rdivmuldivd  13311  subrginv  13356  islmod  13379  lmodlema  13380  islmodd  13381  resttop  13640  restco  13644  restin  13646  lmfval  13662  cnprcl2k  13676  txrest  13746  txdis1cn  13748  cnmpt2res  13767  psmettri2  13798  psmettri  13800  xmettri2  13831  xmettri  13842  mettri  13843  metrtri  13847  blvalps  13858  blval  13859  xblss2  13875  blhalf  13878  comet  13969  xmetxp  13977  txmetcnp  13988  cnmet  14000  ioo2bl  14013  limcmpted  14102  limcimolemlt  14103  cnplimclemr  14108  limccnp2cntop  14116  reldvg  14118  dvfvalap  14120  dvidlemap  14130  dvconst  14131  dvcnp2cntop  14133  dvaddxxbr  14135  dvmulxxbr  14136  dvcoapbr  14141  dvcjbr  14142  dvexp  14145  dvrecap  14147  dvmptcmulcn  14153  dveflem  14157  sin0pilem1  14172  sinperlem  14199  ptolemy  14215  tangtx  14229  abssinper  14237  reexplog  14262  relogexp  14263  cxprec  14301  rpdivcxp  14302  cxpmul  14303  rpabscxpbnd  14329  rplogbval  14333  rplogbreexp  14341  rprelogbmul  14343  logbrec  14348  logbgcd1irraplemap  14357  binom4  14367  lgslem1  14371  lgslem4  14374  lgsval  14375  lgsfvalg  14376  lgsval2lem  14381  lgsval4lem  14382  lgsvalmod  14390  lgsneg  14395  lgsneg1  14396  lgsmod  14397  lgsdilem  14398  lgsdir2lem4  14402  lgsdir2  14404  lgsdirprm  14405  lgsdir  14406  lgsne0  14409  lgssq  14411  lgssq2  14412  lgsmulsqcoprm  14417  lgsdirnn0  14418  lgsdinn0  14419  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  2lgsoddprmlem1  14423  2lgsoddprmlem2  14424  2lgsoddprmlem3  14429  2sqlem1  14431  2sqlem2  14432  mul2sq  14433  2sqlem3  14434  2sqlem4  14435  2sqlem8  14440  2sqlem9  14441  2sqlem10  14442  trilpolemeq1  14758  trilpolemlt1  14759  trirec0xor  14763  apdifflemf  14764  apdiff  14766