Theorem oveq1d 5628

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 5620	. 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 1287  (class class class)co 5613

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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-br 3821  df-iota 4946  df-fv 4989  df-ov 5616

This theorem is referenced by:  csbov2g  5647  caovassg  5760  caovdig  5776  caovdirg  5779  caov12d  5783  caov31d  5784  caov411d  5787  grprinvlem  5796  grprinvd  5797  grpridd  5798  caofinvl  5834  omsuc  6187  nnmsucr  6203  nnm1  6235  nnm2  6236  ecovass  6353  ecoviass  6354  ecovdi  6355  ecovidi  6356  addasspig  6833  mulasspig  6835  mulpipq2  6874  distrnqg  6890  ltsonq  6901  ltanqg  6903  ltmnqg  6904  ltexnqq  6911  archnqq  6920  prarloclemarch2  6922  enq0sym  6935  addnq0mo  6950  mulnq0mo  6951  addnnnq0  6952  nqpnq0nq  6956  nq0m0r  6959  nq0a0  6960  nnanq0  6961  distrnq0  6962  addassnq0  6965  addpinq1  6967  prarloclemlo  6997  prarloclem3  7000  prarloclem5  7003  prarloclemcalc  7005  addnqprllem  7030  addnqprulem  7031  appdivnq  7066  recexprlem1ssl  7136  recexprlem1ssu  7137  ltmprr  7145  cauappcvgprlemladdru  7159  cauappcvgprlem1  7162  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemcl  7179  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlem1  7182  caucvgprprlemcbv  7190  caucvgprprlemval  7191  caucvgprprlemexb  7210  caucvgprprlem1  7212  addcmpblnr  7229  mulcmpblnrlemg  7230  addsrmo  7233  mulsrmo  7234  addsrpr  7235  mulsrpr  7236  ltsrprg  7237  1idsr  7258  pn0sr  7261  recexgt0sr  7263  mulgt0sr  7267  srpospr  7272  prsradd  7275  caucvgsrlemfv  7280  caucvgsrlemcau  7282  caucvgsrlemgt1  7284  caucvgsrlemoffval  7285  caucvgsrlemoffcau  7287  caucvgsrlemoffres  7289  caucvgsrlembnd  7290  caucvgsr  7291  pitonnlem1p1  7327  pitonnlem2  7328  pitonn  7329  recidpirqlemcalc  7338  ax1rid  7356  axrnegex  7358  axcnre  7360  recriota  7369  nntopi  7373  axcaucvglemval  7376  axcaucvglemcau  7377  axcaucvglemres  7378  mul12  7555  mul4  7558  muladd11  7559  readdcan  7566  muladd11r  7582  add12  7584  cnegex  7604  addcan  7606  negeu  7617  pncan2  7633  addsubass  7636  addsub  7637  2addsub  7640  addsubeq4  7641  subid  7645  subid1  7646  npncan  7647  nppcan  7648  nnpcan  7649  nnncan1  7662  npncan3  7664  pnpcan  7665  pnncan  7667  ppncan  7668  addsub4  7669  negsub  7674  subneg  7675  mvlraddd  7789  mvrraddd  7790  subaddeqd  7791  ine0  7816  mulneg1  7817  ltadd2  7841  apreap  8005  cru  8020  recexap  8061  mulcanapd  8069  div23ap  8097  div13ap  8099  divmulassap  8101  divmulasscomap  8102  divcanap4  8105  muldivdirap  8113  divsubdirap  8114  divmuldivap  8118  divdivdivap  8119  divcanap5  8120  divmul13ap  8121  divmuleqap  8123  divdiv32ap  8126  divcanap7  8127  dmdcanap  8128  divdivap1  8129  divdivap2  8130  divadddivap  8133  divsubdivap  8134  conjmulap  8135  divneg2ap  8142  mvllmulapd  8239  lt2mul2div  8275  nndivtr  8398  2halves  8578  halfaddsub  8583  avgle1  8589  avgle2  8590  div4p1lem1div2  8602  un0addcl  8639  un0mulcl  8640  peano2z  8719  zneo  8780  nneoor  8781  nneo  8782  zeo  8784  zeo2  8785  deceq1  8813  qreccl  9059  lincmb01cmp  9352  iccf1o  9353  fzosubel3  9535  qavgle  9598  2tnp1ge0ge0  9636  fldiv4p1lem1div2  9640  ceilqm1lt  9647  flqdiv  9656  modqlt  9668  modqdiffl  9670  modqcyc2  9695  modqaddabs  9697  mulqaddmodid  9699  mulp1mod1  9700  modqmuladd  9701  modqmuladdnn0  9703  qnegmod  9704  addmodid  9707  addmodidr  9708  modqadd2mod  9709  modqm1p1mod0  9710  modqmul12d  9713  modqnegd  9714  modqadd12d  9715  modqsub12d  9716  q2submod  9720  modqmulmodr  9725  modqaddmulmod  9726  modqsubdir  9728  modfzo0difsn  9730  modsumfzodifsn  9731  addmodlteq  9733  frecuzrdgsuc  9749  frecfzennn  9761  iseqovex  9787  iseqoveq  9799  iseq1p  9814  iseqcaopr2  9816  iseqcaopr  9817  iseqid  9843  iseqhomo  9845  iseqz  9846  expp1  9861  exprecap  9895  expaddzaplem  9897  expmulzap  9900  expdivap  9905  sqval  9912  sqsubswap  9914  subsq  9959  subsq2  9960  binom2  9963  binom2sub  9965  mulbinom2  9967  binom3  9968  zesq  9969  bernneq2  9972  sqoddm1div8  10003  nn0opthlem1d  10025  nn0opthd  10027  nn0opth2d  10028  facp1  10035  facdiv  10043  facndiv  10044  faclbnd  10046  faclbnd2  10047  faclbnd3  10048  bcval  10054  bccmpl  10059  bcm1k  10065  bcp1n  10066  bcp1nk  10067  ibcval5  10068  bcp1m1  10070  bcpasc  10071  bcn2m1  10074  hashprg  10113  hashdifpr  10125  hashfzo  10127  hashfzp1  10129  hashfz0  10130  hashxp  10131  zfz1isolemsplit  10140  zfz1isolem1  10142  iseqcoll  10144  reval  10179  crre  10187  remim  10190  remul2  10203  immul2  10210  imval2  10224  cjdivap  10239  caucvgre  10310  cvg1nlemcau  10313  cvg1nlemres  10314  resqrexlemp1rp  10335  resqrexlemfp1  10338  resqrexlemover  10339  resqrexlemcalc1  10343  resqrexlemcalc3  10345  resqrexlemnm  10347  resqrexlemoverl  10350  resqrexlemglsq  10351  resqrexlemga  10352  resqrexlemsqa  10353  resqrexlemex  10354  resqrex  10355  sqrtdiv  10371  absvalsq  10382  absreimsq  10396  absdivap  10399  cau3lem  10443  maxabslemlub  10536  maxabslemval  10537  max0addsup  10548  clim  10564  clim2  10566  climshftlemg  10585  climshft2  10589  climcn1  10591  climcn2  10592  subcn2  10594  climmulc2  10613  climsubc2  10615  clim2iser  10619  climcau  10628  serif0  10633  moddvds  10687  mulmoddvds  10746  3dvds2dec  10748  zeo3  10750  odd2np1lem  10754  odd2np1  10755  oexpneg  10759  2tp1odd  10766  ltoddhalfle  10775  opoe  10777  opeo  10779  omeo  10780  m1expo  10782  m1exp1  10783  nn0o1gt2  10787  nn0o  10789  divalglemnn  10800  divalglemqt  10801  divalglemeunn  10803  divalglemex  10804  divalglemeuneg  10805  flodddiv4  10816  flodddiv4t2lthalf  10819  gcdaddm  10857  bezoutlemnewy  10867  bezoutlema  10870  bezoutlemb  10871  bezoutlemex  10872  bezoutlemaz  10874  mulgcd  10887  gcddiv  10890  gcdmultiplez  10892  rpmulgcd  10897  rplpwr  10898  lcmgcdlem  10941  lcmgcd  10942  divgcdcoprmex  10966  cncongr2  10968  prmexpb  11012  rpexp  11014  rpexp1i  11015  sqrt2irrlem  11022  oddpwdclemxy  11029  oddpwdclemndvds  11031  sqpweven  11035  2sqpwodd  11036  sqne2sq  11037  qmuldeneqnum  11055  nn0gcdsq  11060  zgcdsq  11061  numdensq  11062  dfphi2  11078  phiprmpw  11080  phiprm  11081  hashgcdlem  11085