Theorem oveq1d 5606

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 5598	. 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 1285  (class class class)co 5591

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359  df-v 2614  df-un 2988  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-br 3812  df-iota 4934  df-fv 4977  df-ov 5594

This theorem is referenced by:  csbov2g  5625  caovassg  5738  caovdig  5754  caovdirg  5757  caov12d  5761  caov31d  5762  caov411d  5765  grprinvlem  5774  grprinvd  5775  grpridd  5776  caofinvl  5812  omsuc  6165  nnmsucr  6181  nnm1  6213  nnm2  6214  ecovass  6331  ecoviass  6332  ecovdi  6333  ecovidi  6334  addasspig  6792  mulasspig  6794  mulpipq2  6833  distrnqg  6849  ltsonq  6860  ltanqg  6862  ltmnqg  6863  ltexnqq  6870  archnqq  6879  prarloclemarch2  6881  enq0sym  6894  addnq0mo  6909  mulnq0mo  6910  addnnnq0  6911  nqpnq0nq  6915  nq0m0r  6918  nq0a0  6919  nnanq0  6920  distrnq0  6921  addassnq0  6924  addpinq1  6926  prarloclemlo  6956  prarloclem3  6959  prarloclem5  6962  prarloclemcalc  6964  addnqprllem  6989  addnqprulem  6990  appdivnq  7025  recexprlem1ssl  7095  recexprlem1ssu  7096  ltmprr  7104  cauappcvgprlemladdru  7118  cauappcvgprlem1  7121  caucvgprlemnkj  7128  caucvgprlemnbj  7129  caucvgprlemcl  7138  caucvgprlemladdfu  7139  caucvgprlemladdrl  7140  caucvgprlem1  7141  caucvgprprlemcbv  7149  caucvgprprlemval  7150  caucvgprprlemexb  7169  caucvgprprlem1  7171  addcmpblnr  7188  mulcmpblnrlemg  7189  addsrmo  7192  mulsrmo  7193  addsrpr  7194  mulsrpr  7195  ltsrprg  7196  1idsr  7217  pn0sr  7220  recexgt0sr  7222  mulgt0sr  7226  srpospr  7231  prsradd  7234  caucvgsrlemfv  7239  caucvgsrlemcau  7241  caucvgsrlemgt1  7243  caucvgsrlemoffval  7244  caucvgsrlemoffcau  7246  caucvgsrlemoffres  7248  caucvgsrlembnd  7249  caucvgsr  7250  pitonnlem1p1  7286  pitonnlem2  7287  pitonn  7288  recidpirqlemcalc  7297  ax1rid  7315  axrnegex  7317  axcnre  7319  recriota  7328  nntopi  7332  axcaucvglemval  7335  axcaucvglemcau  7336  axcaucvglemres  7337  mul12  7514  mul4  7517  muladd11  7518  readdcan  7525  muladd11r  7541  add12  7543  cnegex  7563  addcan  7565  negeu  7576  pncan2  7592  addsubass  7595  addsub  7596  2addsub  7599  addsubeq4  7600  subid  7604  subid1  7605  npncan  7606  nppcan  7607  nnpcan  7608  nnncan1  7621  npncan3  7623  pnpcan  7624  pnncan  7626  ppncan  7627  addsub4  7628  negsub  7633  subneg  7634  mvlraddd  7748  mvrraddd  7749  subaddeqd  7750  ine0  7775  mulneg1  7776  ltadd2  7800  apreap  7964  cru  7979  recexap  8020  mulcanapd  8028  div23ap  8056  div13ap  8058  divmulassap  8060  divmulasscomap  8061  divcanap4  8064  muldivdirap  8072  divsubdirap  8073  divmuldivap  8077  divdivdivap  8078  divcanap5  8079  divmul13ap  8080  divmuleqap  8082  divdiv32ap  8085  divcanap7  8086  dmdcanap  8087  divdivap1  8088  divdivap2  8089  divadddivap  8092  divsubdivap  8093  conjmulap  8094  divneg2ap  8101  mvllmulapd  8198  lt2mul2div  8234  nndivtr  8357  2halves  8537  halfaddsub  8542  avgle1  8548  avgle2  8549  div4p1lem1div2  8561  un0addcl  8598  un0mulcl  8599  peano2z  8682  zneo  8743  nneoor  8744  nneo  8745  zeo  8747  zeo2  8748  deceq1  8776  qreccl  9022  lincmb01cmp  9315  iccf1o  9316  fzosubel3  9496  qavgle  9559  2tnp1ge0ge0  9597  fldiv4p1lem1div2  9601  ceilqm1lt  9608  flqdiv  9617  modqlt  9629  modqdiffl  9631  modqcyc2  9656  modqaddabs  9658  mulqaddmodid  9660  mulp1mod1  9661  modqmuladd  9662  modqmuladdnn0  9664  qnegmod  9665  addmodid  9668  addmodidr  9669  modqadd2mod  9670  modqm1p1mod0  9671  modqmul12d  9674  modqnegd  9675  modqadd12d  9676  modqsub12d  9677  q2submod  9681  modqmulmodr  9686  modqaddmulmod  9687  modqsubdir  9689  modfzo0difsn  9691  modsumfzodifsn  9692  addmodlteq  9694  frecuzrdgsuc  9710  frecfzennn  9722  iseqovex  9748  iseqoveq  9759  iseq1p  9774  iseqcaopr2  9776  iseqcaopr  9777  iseqid  9782  iseqhomo  9784  iseqz  9785  expp1  9799  exprecap  9833  expaddzaplem  9835  expmulzap  9838  expdivap  9843  sqval  9850  sqsubswap  9852  subsq  9897  subsq2  9898  binom2  9901  binom2sub  9903  mulbinom2  9905  binom3  9906  zesq  9907  bernneq2  9910  sqoddm1div8  9941  nn0opthlem1d  9963  nn0opthd  9965  nn0opth2d  9966  facp1  9973  facdiv  9981  facndiv  9982  faclbnd  9984  faclbnd2  9985  faclbnd3  9986  bcval  9992  bccmpl  9997  bcm1k  10003  bcp1n  10004  bcp1nk  10005  ibcval5  10006  bcp1m1  10008  bcpasc  10009  bcn2m1  10012  hashprg  10051  hashdifpr  10063  hashfzo  10065  hashfzp1  10067  hashfz0  10068  hashxp  10069  reval  10110  crre  10118  remim  10121  remul2  10134  immul2  10141  imval2  10155  cjdivap  10170  caucvgre  10241  cvg1nlemcau  10244  cvg1nlemres  10245  resqrexlemp1rp  10266  resqrexlemfp1  10269  resqrexlemover  10270  resqrexlemcalc1  10274  resqrexlemcalc3  10276  resqrexlemnm  10278  resqrexlemoverl  10281  resqrexlemglsq  10282  resqrexlemga  10283  resqrexlemsqa  10284  resqrexlemex  10285  resqrex  10286  sqrtdiv  10302  absvalsq  10313  absreimsq  10327  absdivap  10330  cau3lem  10374  maxabslemlub  10467  maxabslemval  10468  max0addsup  10479  clim  10494  clim2  10496  climshftlemg  10515  climshft2  10519  climcn1  10521  climcn2  10522  subcn2  10524  climmulc2  10543  climsubc2  10545  clim2iser  10549  climcau  10558  serif0  10563  moddvds  10585  mulmoddvds  10644  3dvds2dec  10646  zeo3  10648  odd2np1lem  10652  odd2np1  10653  oexpneg  10657  2tp1odd  10664  ltoddhalfle  10673  opoe  10675  opeo  10677  omeo  10678  m1expo  10680  m1exp1  10681  nn0o1gt2  10685  nn0o  10687  divalglemnn  10698  divalglemqt  10699  divalglemeunn  10701  divalglemex  10702  divalglemeuneg  10703  flodddiv4  10714  flodddiv4t2lthalf  10717  gcdaddm  10755  bezoutlemnewy  10765  bezoutlema  10768  bezoutlemb  10769  bezoutlemex  10770  bezoutlemaz  10772  mulgcd  10785  gcddiv  10788  gcdmultiplez  10790  rpmulgcd  10795  rplpwr  10796  lcmgcdlem  10839  lcmgcd  10840  divgcdcoprmex  10864  cncongr2  10866  prmexpb  10910  rpexp  10912  rpexp1i  10913  sqrt2irrlem  10920  oddpwdclemxy  10927  oddpwdclemndvds  10929  sqpweven  10933  2sqpwodd  10934  sqne2sq  10935  qmuldeneqnum  10953  nn0gcdsq  10958  zgcdsq  10959  numdensq  10960  dfphi2  10976  phiprmpw  10978  phiprm  10979  hashgcdlem  10983