Theorem oveq1d 5884

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 5876	. 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 5869

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 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-iota 5174  df-fv 5220  df-ov 5872

This theorem is referenced by:  fvoveq1d  5891  csbov2g  5910  caovassg  6027  caovdig  6043  caovdirg  6046  caov12d  6050  caov31d  6051  caov411d  6054  caofinvl  6099  omsuc  6467  nnmsucr  6483  nnm1  6520  nnm2  6521  ecovass  6638  ecoviass  6639  ecovdi  6640  ecovidi  6641  addasspig  7320  mulasspig  7322  mulpipq2  7361  distrnqg  7377  ltsonq  7388  ltanqg  7390  ltmnqg  7391  ltexnqq  7398  archnqq  7407  prarloclemarch2  7409  enq0sym  7422  addnq0mo  7437  mulnq0mo  7438  addnnnq0  7439  nqpnq0nq  7443  nq0m0r  7446  nq0a0  7447  nnanq0  7448  distrnq0  7449  addassnq0  7452  addpinq1  7454  prarloclemlo  7484  prarloclem3  7487  prarloclem5  7490  prarloclemcalc  7492  addnqprllem  7517  addnqprulem  7518  appdivnq  7553  recexprlem1ssl  7623  recexprlem1ssu  7624  ltmprr  7632  cauappcvgprlemladdru  7646  cauappcvgprlem1  7649  caucvgprlemnkj  7656  caucvgprlemnbj  7657  caucvgprlemcl  7666  caucvgprlemladdfu  7667  caucvgprlemladdrl  7668  caucvgprlem1  7669  caucvgprprlemcbv  7677  caucvgprprlemval  7678  caucvgprprlemexb  7697  caucvgprprlem1  7699  addcmpblnr  7729  mulcmpblnrlemg  7730  addsrmo  7733  mulsrmo  7734  addsrpr  7735  mulsrpr  7736  ltsrprg  7737  1idsr  7758  pn0sr  7761  recexgt0sr  7763  mulgt0sr  7768  srpospr  7773  prsradd  7776  caucvgsrlemfv  7781  caucvgsrlemcau  7783  caucvgsrlemgt1  7785  caucvgsrlemoffval  7786  caucvgsrlemoffcau  7788  caucvgsrlemoffres  7790  caucvgsrlembnd  7791  caucvgsr  7792  map2psrprg  7795  pitonnlem1p1  7836  pitonnlem2  7837  pitonn  7838  recidpirqlemcalc  7847  ax1rid  7867  axrnegex  7869  axcnre  7871  recriota  7880  nntopi  7884  axcaucvglemval  7887  axcaucvglemcau  7888  axcaucvglemres  7889  mul12  8076  mul4  8079  muladd11  8080  readdcan  8087  muladd11r  8103  add12  8105  cnegex  8125  addcan  8127  negeu  8138  pncan2  8154  addsubass  8157  addsub  8158  2addsub  8161  addsubeq4  8162  subid  8166  subid1  8167  npncan  8168  nppcan  8169  nnpcan  8170  nnncan1  8183  npncan3  8185  pnpcan  8186  pnncan  8188  ppncan  8189  addsub4  8190  negsub  8195  subneg  8196  subeqxfrd  8310  mvlraddd  8311  mvlladdd  8312  mvrraddd  8313  subaddeqd  8316  ine0  8341  mulneg1  8342  ltadd2  8366  apreap  8534  cru  8549  recexap  8599  mulcanapd  8607  div23ap  8637  div13ap  8639  divmulassap  8641  divmulasscomap  8642  divcanap4  8645  muldivdirap  8653  divsubdirap  8654  divmuldivap  8658  divdivdivap  8659  divcanap5  8660  divmul13ap  8661  divmuleqap  8663  divdiv32ap  8666  divcanap7  8667  dmdcanap  8668  divdivap1  8669  divdivap2  8670  divadddivap  8673  divsubdivap  8674  conjmulap  8675  divneg2ap  8682  subrecap  8785  mvllmulapd  8788  lt2mul2div  8825  nndivtr  8950  2halves  9137  halfaddsub  9142  avgle1  9148  avgle2  9149  div4p1lem1div2  9161  un0addcl  9198  un0mulcl  9199  peano2z  9278  zneo  9343  nneoor  9344  nneo  9345  zeo  9347  zeo2  9348  deceq1  9377  qreccl  9631  xaddcom  9848  xnegdi  9855  xaddass  9856  xaddass2  9857  xpncan  9858  xleadd1a  9860  xltadd1  9863  xposdif  9869  xadd4d  9872  lincmb01cmp  9990  iccf1o  9991  fz0to4untppr  10110  fzosubel3  10182  qavgle  10245  2tnp1ge0ge0  10287  fldiv4p1lem1div2  10291  ceilqm1lt  10298  flqdiv  10307  modqlt  10319  modqdiffl  10321  modqcyc2  10346  modqaddabs  10348  mulqaddmodid  10350  mulp1mod1  10351  modqmuladd  10352  modqmuladdnn0  10354  qnegmod  10355  addmodid  10358  addmodidr  10359  modqadd2mod  10360  modqm1p1mod0  10361  modqmul12d  10364  modqnegd  10365  modqadd12d  10366  modqsub12d  10367  q2submod  10371  modqmulmodr  10376  modqaddmulmod  10377  modqsubdir  10379  modfzo0difsn  10381  modsumfzodifsn  10382  addmodlteq  10384  frecuzrdgsuc  10400  frecfzennn  10412  iseqovex  10442  seq3-1p  10466  seq3caopr2  10468  seq3caopr  10469  seq3id  10494  seq3homo  10496  seq3z  10497  expp1  10513  exprecap  10547  expaddzaplem  10549  expmulzap  10552  expdivap  10557  sqval  10564  sqsubswap  10566  subsq  10612  subsq2  10613  binom2  10617  binom2sub  10619  mulbinom2  10622  binom3  10623  zesq  10624  bernneq2  10627  modqexp  10632  sqoddm1div8  10659  nn0opthlem1d  10684  nn0opthd  10686  nn0opth2d  10687  facp1  10694  facdiv  10702  facndiv  10703  faclbnd  10705  faclbnd2  10706  faclbnd3  10707  bcval  10713  bccmpl  10718  bcm1k  10724  bcp1n  10725  bcp1nk  10726  bcval5  10727  bcp1m1  10729  bcpasc  10730  bcn2m1  10733  hashprg  10772  hashdifpr  10784  hashfzo  10786  hashfzp1  10788  hashfz0  10789  hashxp  10790  zfz1isolemsplit  10802  zfz1isolem1  10804  seq3coll  10806  reval  10842  crre  10850  remim  10853  remul2  10866  immul2  10873  imval2  10887  cjdivap  10902  caucvgre  10974  cvg1nlemcau  10977  cvg1nlemres  10978  resqrexlemp1rp  10999  resqrexlemfp1  11002  resqrexlemover  11003  resqrexlemcalc1  11007  resqrexlemcalc3  11009  resqrexlemnm  11011  resqrexlemoverl  11014  resqrexlemglsq  11015  resqrexlemga  11016  resqrexlemsqa  11017  resqrexlemex  11018  resqrex  11019  sqrtdiv  11035  absvalsq  11046  absreimsq  11060  absdivap  11063  cau3lem  11107  maxabslemlub  11200  maxabslemval  11201  max0addsup  11212  minabs  11228  bdtrilem  11231  bdtri  11232  xrmaxaddlem  11252  xrmaxadd  11253  xrbdtri  11268  clim  11273  clim2  11275  climshftlemg  11294  climshft2  11298  climcn1  11300  climcn2  11301  subcn2  11303  reccn2ap  11305  climmulc2  11323  climsubc2  11325  clim2ser  11329  iser3shft  11338  climcau  11339  serf0  11344  fzosump1  11409  fsum1p  11410  fsump1  11412  sumsplitdc  11424  fsump1i  11425  mptfzshft  11434  fisum0diag2  11439  fsumconst  11446  fsumdifsnconst  11447  modfsummodlemstep  11449  modfsummod  11450  telfsumo  11458  fsumparts  11462  fsumrelem  11463  hash2iun1dif1  11472  binomlem  11475  binom  11476  binom1p  11477  binom1dif  11479  bcxmas  11481  isumsplit  11483  isum1p  11484  arisum  11490  arisum2  11491  trireciplem  11492  geoserap  11499  geolim  11503  geolim2  11504  georeclim  11505  geo2sum  11506  geoisum1  11511  cvgratnnlemseq  11518  cvgratnnlemsumlt  11520  cvgratnnlemfm  11521  cvgratz  11524  mertenslemi1  11527  mertenslem2  11528  mertensabs  11529  fprod1p  11591  fprodp1  11592  fprodcl2lem  11597  fprodfac  11607  fprodeq0  11609  fprodconst  11612  fprodrec  11621  fprodsplit1f  11626  fprodmodd  11633  efcllemp  11650  ef0lem  11652  efval  11653  esum  11654  ege2le3  11663  efaddlem  11666  efsep  11683  effsumlt  11684  eft0val  11685  efgt1p2  11687  efgt1p  11688  sinval  11694  cosval  11695  resinval  11707  recosval  11708  efi4p  11709  resin4p  11710  recos4p  11711  sinneg  11718  cosneg  11719  efival  11724  sinadd  11728  cosadd  11729  tanaddap  11731  sinmul  11736  cosmul  11737  cos2t  11742  cos2tsin  11743  ef01bndlem  11748  absefib  11762  demoivre  11764  demoivreALT  11765  eirraplem  11768  p1modz1  11785  dvdsmodexp  11786  moddvds  11790  mulmoddvds  11852  3dvds2dec  11854  zeo3  11856  odd2np1lem  11860  odd2np1  11861  oexpneg  11865  2tp1odd  11872  ltoddhalfle  11881  opoe  11883  opeo  11885  omeo  11886  m1expo  11888  m1exp1  11889  nn0o1gt2  11893  nn0o  11895  divalglemnn  11906  divalglemqt  11907  divalglemeunn  11909  divalglemex  11910  divalglemeuneg  11911  flodddiv4  11922  flodddiv4t2lthalf  11925  gcdaddm  11968  bezoutlemnewy  11980  bezoutlema  11983  bezoutlemb  11984  bezoutlemex  11985  bezoutlemaz  11987  mulgcd  12000  gcddiv  12003  gcdmultiplez  12005  rpmulgcd  12010  rplpwr  12011  uzwodc  12021  lcmgcdlem  12060  lcmgcd  12061  divgcdcoprmex  12085  cncongr2  12087  prmexpb  12134  rpexp  12136  rpexp1i  12137  sqrt2irrlem  12144  oddpwdclemxy  12152  oddpwdclemndvds  12154  sqpweven  12158  2sqpwodd  12159  sqne2sq  12160  qmuldeneqnum  12178  nn0gcdsq  12183  zgcdsq  12184  numdensq  12185  dfphi2  12203  phiprmpw  12205  phiprm  12206  eulerthlema  12213  eulerthlemh  12214  eulerthlemth  12215  fermltl  12217  prmdiv  12218  prmdiveq  12219  prmdivdiv  12220  hashgcdlem  12221  odzval  12224  odzcllem  12225  odzdvds  12228  vfermltl  12234  powm2modprm  12235  reumodprminv  12236  modprm0  12237  nnnn0modprm0  12238  modprmn0modprm0  12239  coprimeprodsq  12240  coprimeprodsq2  12241  pythagtriplem1  12248  pythagtriplem3  12250  pythagtriplem4  12251  pythagtriplem6  12253  pythagtriplem7  12254  pythagtriplem12  12258  pythagtriplem14  12260  pythagtriplem15  12261  pythagtriplem16  12262  pythagtriplem17  12263  pythagtriplem18  12264  pceu  12278  pczpre  12280  pcdiv  12285  pcqdiv  12290  pcrec  12291  pczndvds  12298  pcneg  12307  pc2dvds  12312  pcprmpw2  12315  pcaddlem  12321  pcadd  12322  fldivp1  12329  pockthlem  12337  pockthi  12339  4sqlem5  12363  4sqlem9  12367  4sqlem10  12368  4sqlem2  12370  4sqlem3  12371  4sqlem4  12373  mul4sqlem  12374  ennnfonelemkh  12396  ennnfonelemhf1o  12397  ressressg  12516  grprinvlem  12696  grprinvd  12697  grpridd  12698  isnsgrp  12704  sgrpass  12706  sgrp1  12708  mnd12g  12721  mndpropd  12733  mhmlin  12748  grprcan  12800  grpinvid1  12814  isgrpinv  12816  grplcan  12821  grpasscan1  12822  grplmulf1o  12833  grpinvadd  12837  grpinvsub  12841  grpsubsub4  12852  grppnpcan2  12853  grpnpncan  12854  dfgrp3mlem  12857  dfgrp3m  12858  grplactcnv  12861  mhmlem  12867  mhmid  12868  mhmmnd  12869  mulgnnp1  12880  mulg2  12881  mulgnn0p1  12883  mulgsubcl  12886  mulgneg  12890  mulgaddcomlem  12894  mulgaddcom  12895  mulgz  12899  mulgnn0dir  12901  mulgdirlem  12902  mulgdir  12903  mulgneg2  12905  mulgnnass  12906  mulgnn0ass  12907  mulgass  12908  mulgassr  12909  mulgmodid  12910  mulgsubdir  12911  ablsub2inv  12941  abladdsub4  12944  abladdsub  12945  ablpncan2  12946  ablpnpcan  12950  ablnncan  12951  ablnnncan1  12954  srgass  12980  srgmulgass  12998  srgpcomp  12999  srgpcompp  13000  srgpcomppsc  13001  ringpropd  13043  ringlz  13048  ring1eq0  13051  ringnegl  13054  ringmneg1  13056  rngsubdir  13060  mulgass2  13061  ring1  13062  opprring  13074  unitgrp  13110  dvrcan1  13134  resttop  13337  restco  13341  restin  13343  lmfval  13359  cnprcl2k  13373  txrest  13443  txdis1cn  13445  cnmpt2res  13464  psmettri2  13495  psmettri  13497  xmettri2  13528  xmettri  13539  mettri  13540  metrtri  13544  blvalps  13555  blval  13556  xblss2  13572  blhalf  13575  comet  13666  xmetxp  13674  txmetcnp  13685  cnmet  13697  ioo2bl  13710  limcmpted  13799  limcimolemlt  13800  cnplimclemr  13805  limccnp2cntop  13813  reldvg  13815  dvfvalap  13817  dvidlemap  13827  dvconst  13828  dvcnp2cntop  13830  dvaddxxbr  13832  dvmulxxbr  13833  dvcoapbr  13838  dvcjbr  13839  dvexp  13842  dvrecap  13844  dvmptcmulcn  13850  dveflem  13854  sin0pilem1  13869  sinperlem  13896  ptolemy  13912  tangtx  13926  abssinper  13934  reexplog  13959  relogexp  13960  cxprec  13998  rpdivcxp  13999  cxpmul  14000  rpabscxpbnd  14026  rplogbval  14030  rplogbreexp  14038  rprelogbmul  14040  logbrec  14045  logbgcd1irraplemap  14054  binom4  14064  lgslem1  14068  lgslem4  14071  lgsval  14072  lgsfvalg  14073  lgsval2lem  14078  lgsval4lem  14079  lgsvalmod  14087  lgsneg  14092  lgsneg1  14093  lgsmod  14094  lgsdilem  14095  lgsdir2lem4  14099  lgsdir2  14101  lgsdirprm  14102  lgsdir  14103  lgsne0  14106  lgssq  14108  lgssq2  14109  lgsmulsqcoprm  14114  lgsdirnn0  14115  lgsdinn0  14116  2sqlem1  14117  2sqlem2  14118  mul2sq  14119  2sqlem3  14120  2sqlem4  14121  2sqlem8  14126  2sqlem9  14127  2sqlem10  14128  trilpolemeq1  14444  trilpolemlt1  14445  trirec0xor  14449  apdifflemf  14450  apdiff  14452