Theorem oveq2d 5631

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)

Hypothesis

Ref	Expression
oveq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
oveq2d	|- ( ph -> ( C F A ) = ( C F B ) )

Proof of Theorem oveq2d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		oveq2 5623	. 2 |- ( A = B -> ( C F A ) = ( C F B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1287  (class class class)co 5615

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 3639  df-br 3823  df-iota 4948  df-fv 4991  df-ov 5618

This theorem is referenced by:  csbov1g  5648  caovassg  5762  caovdig  5778  caovdirg  5781  caov32d  5784  caov4d  5788  caov42d  5790  grprinvlem  5798  grprinvd  5799  grpridd  5800  nnaass  6202  nndi  6203  nnmass  6204  nnmsucr  6205  ecovass  6355  ecoviass  6356  ecovdi  6357  ecovidi  6358  addasspig  6836  mulasspig  6838  distrpig  6839  dfplpq2  6860  mulpipq2  6877  addassnqg  6888  prarloclemarch  6924  prarloclemarch2  6925  ltrnqg  6926  enq0sym  6938  addnq0mo  6953  mulnq0mo  6954  addnnnq0  6955  nq0a0  6963  distrnq0  6965  addassnq0  6968  prarloclemlo  7000  prarloclem3  7003  prarloclem5  7006  prarloclemcalc  7008  addnqprl  7035  addnqpru  7036  prmuloclemcalc  7071  mulnqprl  7074  mulnqpru  7075  distrlem4prl  7090  distrlem4pru  7091  1idprl  7096  1idpru  7097  ltexprlemloc  7113  addcanprleml  7120  addcanprlemu  7121  recexprlem1ssu  7140  ltmprr  7148  caucvgprlemcanl  7150  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgprlem1  7165  cauappcvgprlemlim  7167  caucvgprlemnkj  7172  caucvgprlemnbj  7173  caucvgprlemdisj  7180  caucvgprlemloc  7181  caucvgprlemcl  7182  caucvgprlemladdrl  7184  caucvgprlem1  7185  caucvgpr  7188  caucvgprprlemell  7191  caucvgprprlemcbv  7193  caucvgprprlemval  7194  caucvgprprlemnkeqj  7196  caucvgprprlemopl  7203  caucvgprprlemlol  7204  caucvgprprlemloc  7209  caucvgprprlemclphr  7211  caucvgprprlemexb  7213  caucvgprprlemaddq  7214  caucvgprprlem1  7215  addcmpblnr  7232  mulcmpblnrlemg  7233  addsrmo  7236  mulsrmo  7237  addsrpr  7238  mulsrpr  7239  ltsrprg  7240  recexgt0sr  7266  mulgt0sr  7270  caucvgsrlemgt1  7287  caucvgsrlemoffval  7288  caucvgsr  7294  mulcnsr  7319  pitoregt0  7333  recidpirqlemcalc  7341  axmulcom  7353  axmulass  7355  axdistr  7356  ax0id  7360  axcnre  7363  recriota  7372  axcaucvglemcau  7380  axcaucvglemres  7381  mulid1  7432  adddirp1d  7461  mul32  7559  mul31  7560  add32  7588  add4  7590  add42  7591  cnegex  7607  addcan2  7610  addsubass  7639  subsub2  7657  nppcan2  7660  sub32  7663  nnncan  7664  sub4  7674  muladd  7809  subdi  7810  mul2neg  7823  submul2  7824  mulsub  7826  mulsubfacd  7843  add20  7899  recexre  7999  rereim  8007  apreap  8008  ltmul1  8013  cru  8023  apreim  8024  mulreim  8025  apadd1  8029  apneg  8032  mulap0  8065  divrecap  8097  divassap  8099  divmulasscomap  8105  divsubdirap  8117  divdivdivap  8122  divmul24ap  8125  divmuleqap  8126  divcanap6  8128  divdivap1  8132  divdivap2  8133  divsubdivap  8137  conjmulap  8138  div2negap  8144  apmul1  8197  cju  8359  nnmulcl  8381  add1p1  8601  sub1m1  8602  cnm2m1cnm3  8603  xp1d2m1eqxm1d2  8604  div4p1lem1div2  8605  un0addcl  8642  un0mulcl  8643  zaddcllemneg  8725  qapne  9059  cnref1o  9068  lincmb01cmp  9355  iccf1o  9356  ige3m2fz  9398  fztp  9425  fzsuc2  9426  fseq1m1p1  9442  fzm1  9447  ige2m1fz1  9456  nn0split  9478  nnsplit  9479  fzval3  9546  zpnn0elfzo1  9550  fzosplitsnm1  9551  fzosplitprm1  9576  fzoshftral  9580  rebtwn2zlemstep  9595  flhalf  9640  modqval  9662  modqvalr  9663  modqdiffl  9673  modqfrac  9675  flqmod  9676  intqfrac  9677  zmod10  9678  modqmulnn  9680  modqvalp1  9681  modqid  9687  modqcyc  9697  modqcyc2  9698  modqmul1  9715  q2submod  9723  modqdi  9730  modqsubdir  9731  modqeqmodmin  9732  modsumfzodifsn  9734  addmodlteq  9736  frecuzrdgsuctlem  9761  uzsinds  9779  iseqeq3  9787  iseqval  9791  iseqvalcbv  9792  iseqvalt  9793  iseqfclt  9797  iseqp1  9799  iseqp1t  9800  iseqm1  9805  iseqfveq2  9806  iseqshft2  9810  monoord2  9814  isermono  9815  iseqsplit  9816  iseqcaopr3  9818  iseqcaopr2  9819  iseqcaopr  9820  iseqid2  9847  iseqhomo  9848  iseqz  9849  expivallem  9858  expival  9859  expp1  9864  expnegap0  9865  expineg2  9866  expn1ap0  9867  expm1t  9885  1exp  9886  expnegzap  9891  mulexpzap  9897  expadd  9899  expaddzaplem  9900  expaddzap  9901  expmul  9902  expmulzap  9903  m1expeven  9904  expsubap  9905  expp1zap  9906  expm1ap  9907  expdivap  9908  iexpcyc  9960  subsq2  9963  binom2  9966  binom21  9967  binom2sub  9968  mulbinom2  9970  binom3  9971  zesq  9972  bernneq  9974  sqoddm1div8  10006  nn0opthlem1d  10028  nn0opthd  10030  facp1  10038  facnn2  10042  faclbnd  10049  faclbnd6  10052  bcval  10057  bccmpl  10062  bcn0  10063  bcnn  10065  bcnp1n  10067  bcm1k  10068  bcp1n  10069  bcp1nk  10070  ibcval5  10071  bcp1m1  10073  bcpasc  10074  bcn2m1  10077  bcn2p1  10078  omgadd  10110  hashunlem  10112  hashunsng  10115  hashdifsn  10127  hashxp  10134  zfz1isolemsplit  10143  zfz1isolem1  10145  zfz1iso  10146  iseqcoll  10147  shftcan1  10168  shftcan2  10169  cjval  10178  cjth  10179  crre  10190  replim  10192  remim  10193  reim0b  10195  rereb  10196  mulreap  10197  cjreb  10199  recj  10200  reneg  10201  readd  10202  resub  10203  remullem  10204  imcj  10208  imneg  10209  imadd  10210  imsub  10211  cjcj  10216  cjadd  10217  ipcnval  10219  cjmulrcl  10220  cjneg  10223  addcj  10224  cjsub  10225  cnrecnv  10243  caucvgrelemcau  10312  cvg1nlemcau  10316  cvg1nlemres  10317  recvguniqlem  10326  resqrexlemover  10342  resqrexlemlo  10345  resqrexlemcalc1  10346  resqrexlemcalc3  10348  resqrexlemnm  10350  resqrexlemcvg  10351  absneg  10382  abscj  10384  sqabsadd  10387  sqabssub  10388  absmul  10401  absid  10403  absre  10409  absresq  10410  absexpzap  10412  recvalap  10429  abstri  10436  abs2dif2  10439  recan  10441  cau3lem  10446  amgm2  10450  climaddc1  10614  climsubc1  10617  climcvg1nlem  10633  serif0  10636  isummolem3  10664  isummolem2a  10665  isummo  10667  fsumm1  10697  fsumsplitsnun  10700  fsump1  10701  dvdsexp  10768  oexpneg  10783  opeo  10803  omeo  10804  m1exp1  10807  flodddiv4  10840  flodddiv4t2lthalf  10843  divgcdnnr  10873  gcdaddm  10881  gcdadd  10882  gcdid  10883  modgcd  10888  bezoutlemnewy  10891  bezoutlema  10894  bezoutlemb  10895  bezoutlemex  10896  bezoutlembz  10899  absmulgcd  10912  gcdmultiple  10915  gcdmultiplez  10916  rpmulgcd  10921  rplpwr  10922  eucalginv  10944  eucialg  10947  lcmneg  10962  lcmgcdlem  10965  lcmgcd  10966  lcmid  10968  lcm1  10969  mulgcddvds  10982  qredeq  10984  divgcdcoprmex  10990  prmind2  11008  rpexp1i  11039  pw2dvdslemn  11049  pw2dvdseulemle  11051  pw2dvdseu  11052  oddpwdclemxy  11053  oddpwdclemdvds  11054  oddpwdclemndvds  11055  oddpwdclemdc  11057  2sqpwodd  11060  nn0gcdsq  11084  phiprmpw  11104  hashgcdlem  11109  qdencn  11384