Theorem oveq1d 5789

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 5781	. 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 1331  (class class class)co 5774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777

This theorem is referenced by:  fvoveq1d  5796  csbov2g  5812  caovassg  5929  caovdig  5945  caovdirg  5948  caov12d  5952  caov31d  5953  caov411d  5956  grprinvlem  5965  grprinvd  5966  grpridd  5967  caofinvl  6004  omsuc  6368  nnmsucr  6384  nnm1  6420  nnm2  6421  ecovass  6538  ecoviass  6539  ecovdi  6540  ecovidi  6541  addasspig  7138  mulasspig  7140  mulpipq2  7179  distrnqg  7195  ltsonq  7206  ltanqg  7208  ltmnqg  7209  ltexnqq  7216  archnqq  7225  prarloclemarch2  7227  enq0sym  7240  addnq0mo  7255  mulnq0mo  7256  addnnnq0  7257  nqpnq0nq  7261  nq0m0r  7264  nq0a0  7265  nnanq0  7266  distrnq0  7267  addassnq0  7270  addpinq1  7272  prarloclemlo  7302  prarloclem3  7305  prarloclem5  7308  prarloclemcalc  7310  addnqprllem  7335  addnqprulem  7336  appdivnq  7371  recexprlem1ssl  7441  recexprlem1ssu  7442  ltmprr  7450  cauappcvgprlemladdru  7464  cauappcvgprlem1  7467  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemcl  7484  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlem1  7487  caucvgprprlemcbv  7495  caucvgprprlemval  7496  caucvgprprlemexb  7515  caucvgprprlem1  7517  addcmpblnr  7547  mulcmpblnrlemg  7548  addsrmo  7551  mulsrmo  7552  addsrpr  7553  mulsrpr  7554  ltsrprg  7555  1idsr  7576  pn0sr  7579  recexgt0sr  7581  mulgt0sr  7586  srpospr  7591  prsradd  7594  caucvgsrlemfv  7599  caucvgsrlemcau  7601  caucvgsrlemgt1  7603  caucvgsrlemoffval  7604  caucvgsrlemoffcau  7606  caucvgsrlemoffres  7608  caucvgsrlembnd  7609  caucvgsr  7610  map2psrprg  7613  pitonnlem1p1  7654  pitonnlem2  7655  pitonn  7656  recidpirqlemcalc  7665  ax1rid  7685  axrnegex  7687  axcnre  7689  recriota  7698  nntopi  7702  axcaucvglemval  7705  axcaucvglemcau  7706  axcaucvglemres  7707  mul12  7891  mul4  7894  muladd11  7895  readdcan  7902  muladd11r  7918  add12  7920  cnegex  7940  addcan  7942  negeu  7953  pncan2  7969  addsubass  7972  addsub  7973  2addsub  7976  addsubeq4  7977  subid  7981  subid1  7982  npncan  7983  nppcan  7984  nnpcan  7985  nnncan1  7998  npncan3  8000  pnpcan  8001  pnncan  8003  ppncan  8004  addsub4  8005  negsub  8010  subneg  8011  subeqxfrd  8125  mvlraddd  8126  mvlladdd  8127  mvrraddd  8128  subaddeqd  8131  ine0  8156  mulneg1  8157  ltadd2  8181  apreap  8349  cru  8364  recexap  8414  mulcanapd  8422  div23ap  8451  div13ap  8453  divmulassap  8455  divmulasscomap  8456  divcanap4  8459  muldivdirap  8467  divsubdirap  8468  divmuldivap  8472  divdivdivap  8473  divcanap5  8474  divmul13ap  8475  divmuleqap  8477  divdiv32ap  8480  divcanap7  8481  dmdcanap  8482  divdivap1  8483  divdivap2  8484  divadddivap  8487  divsubdivap  8488  conjmulap  8489  divneg2ap  8496  subrecap  8598  mvllmulapd  8601  lt2mul2div  8637  nndivtr  8762  2halves  8949  halfaddsub  8954  avgle1  8960  avgle2  8961  div4p1lem1div2  8973  un0addcl  9010  un0mulcl  9011  peano2z  9090  zneo  9152  nneoor  9153  nneo  9154  zeo  9156  zeo2  9157  deceq1  9186  qreccl  9434  xaddcom  9644  xnegdi  9651  xaddass  9652  xaddass2  9653  xpncan  9654  xleadd1a  9656  xltadd1  9659  xposdif  9665  xadd4d  9668  lincmb01cmp  9786  iccf1o  9787  fzosubel3  9973  qavgle  10036  2tnp1ge0ge0  10074  fldiv4p1lem1div2  10078  ceilqm1lt  10085  flqdiv  10094  modqlt  10106  modqdiffl  10108  modqcyc2  10133  modqaddabs  10135  mulqaddmodid  10137  mulp1mod1  10138  modqmuladd  10139  modqmuladdnn0  10141  qnegmod  10142  addmodid  10145  addmodidr  10146  modqadd2mod  10147  modqm1p1mod0  10148  modqmul12d  10151  modqnegd  10152  modqadd12d  10153  modqsub12d  10154  q2submod  10158  modqmulmodr  10163  modqaddmulmod  10164  modqsubdir  10166  modfzo0difsn  10168  modsumfzodifsn  10169  addmodlteq  10171  frecuzrdgsuc  10187  frecfzennn  10199  iseqovex  10229  seq3-1p  10253  seq3caopr2  10255  seq3caopr  10256  seq3id  10281  seq3homo  10283  seq3z  10284  expp1  10300  exprecap  10334  expaddzaplem  10336  expmulzap  10339  expdivap  10344  sqval  10351  sqsubswap  10353  subsq  10399  subsq2  10400  binom2  10403  binom2sub  10405  mulbinom2  10408  binom3  10409  zesq  10410  bernneq2  10413  sqoddm1div8  10444  nn0opthlem1d  10466  nn0opthd  10468  nn0opth2d  10469  facp1  10476  facdiv  10484  facndiv  10485  faclbnd  10487  faclbnd2  10488  faclbnd3  10489  bcval  10495  bccmpl  10500  bcm1k  10506  bcp1n  10507  bcp1nk  10508  bcval5  10509  bcp1m1  10511  bcpasc  10512  bcn2m1  10515  hashprg  10554  hashdifpr  10566  hashfzo  10568  hashfzp1  10570  hashfz0  10571  hashxp  10572  zfz1isolemsplit  10581  zfz1isolem1  10583  seq3coll  10585  reval  10621  crre  10629  remim  10632  remul2  10645  immul2  10652  imval2  10666  cjdivap  10681  caucvgre  10753  cvg1nlemcau  10756  cvg1nlemres  10757  resqrexlemp1rp  10778  resqrexlemfp1  10781  resqrexlemover  10782  resqrexlemcalc1  10786  resqrexlemcalc3  10788  resqrexlemnm  10790  resqrexlemoverl  10793  resqrexlemglsq  10794  resqrexlemga  10795  resqrexlemsqa  10796  resqrexlemex  10797  resqrex  10798  sqrtdiv  10814  absvalsq  10825  absreimsq  10839  absdivap  10842  cau3lem  10886  maxabslemlub  10979  maxabslemval  10980  max0addsup  10991  minabs  11007  bdtrilem  11010  bdtri  11011  xrmaxaddlem  11029  xrmaxadd  11030  xrbdtri  11045  clim  11050  clim2  11052  climshftlemg  11071  climshft2  11075  climcn1  11077  climcn2  11078  subcn2  11080  reccn2ap  11082  climmulc2  11100  climsubc2  11102  clim2ser  11106  iser3shft  11115  climcau  11116  serf0  11121  fzosump1  11186  fsum1p  11187  fsump1  11189  sumsplitdc  11201  fsump1i  11202  mptfzshft  11211  fisum0diag2  11216  fsumconst  11223  fsumdifsnconst  11224  modfsummodlemstep  11226  modfsummod  11227  telfsumo  11235  fsumparts  11239  fsumrelem  11240  hash2iun1dif1  11249  binomlem  11252  binom  11253  binom1p  11254  binom1dif  11256  bcxmas  11258  isumsplit  11260  isum1p  11261  arisum  11267  arisum2  11268  trireciplem  11269  geoserap  11276  geolim  11280  geolim2  11281  georeclim  11282  geo2sum  11283  geoisum1  11288  cvgratnnlemseq  11295  cvgratnnlemsumlt  11297  cvgratnnlemfm  11298  cvgratz  11301  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  efcllemp  11364  ef0lem  11366  efval  11367  esum  11368  ege2le3  11377  efaddlem  11380  efsep  11397  effsumlt  11398  eft0val  11399  efgt1p2  11401  efgt1p  11402  sinval  11409  cosval  11410  resinval  11422  recosval  11423  efi4p  11424  resin4p  11425  recos4p  11426  sinneg  11433  cosneg  11434  efival  11439  sinadd  11443  cosadd  11444  tanaddap  11446  sinmul  11451  cosmul  11452  cos2t  11457  cos2tsin  11458  ef01bndlem  11463  absefib  11477  demoivre  11479  demoivreALT  11480  eirraplem  11483  moddvds  11502  mulmoddvds  11561  3dvds2dec  11563  zeo3  11565  odd2np1lem  11569  odd2np1  11570  oexpneg  11574  2tp1odd  11581  ltoddhalfle  11590  opoe  11592  opeo  11594  omeo  11595  m1expo  11597  m1exp1  11598  nn0o1gt2  11602  nn0o  11604  divalglemnn  11615  divalglemqt  11616  divalglemeunn  11618  divalglemex  11619  divalglemeuneg  11620  flodddiv4  11631  flodddiv4t2lthalf  11634  gcdaddm  11672  bezoutlemnewy  11684  bezoutlema  11687  bezoutlemb  11688  bezoutlemex  11689  bezoutlemaz  11691  mulgcd  11704  gcddiv  11707  gcdmultiplez  11709  rpmulgcd  11714  rplpwr  11715  lcmgcdlem  11758  lcmgcd  11759  divgcdcoprmex  11783  cncongr2  11785  prmexpb  11829  rpexp  11831  rpexp1i  11832  sqrt2irrlem  11839  oddpwdclemxy  11847  oddpwdclemndvds  11849  sqpweven  11853  2sqpwodd  11854  sqne2sq  11855  qmuldeneqnum  11873  nn0gcdsq  11878  zgcdsq  11879  numdensq  11880  dfphi2  11896  phiprmpw  11898  phiprm  11899  hashgcdlem  11903  ennnfonelemkh  11925  ennnfonelemhf1o  11926  resttop  12339  restco  12343  restin  12345  lmfval  12361  cnprcl2k  12375  txrest  12445  txdis1cn  12447  cnmpt2res  12466  psmettri2  12497  psmettri  12499  xmettri2  12530  xmettri  12541  mettri  12542  metrtri  12546  blvalps  12557  blval  12558  xblss2  12574  blhalf  12577  comet  12668  xmetxp  12676  txmetcnp  12687  cnmet  12699  ioo2bl  12712  limcmpted  12801  limcimolemlt  12802  cnplimclemr  12807  limccnp2cntop  12815  reldvg  12817  dvfvalap  12819  dvidlemap  12829  dvconst  12830  dvcnp2cntop  12832  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840  dvcjbr  12841  dvexp  12844  dvrecap  12846  dvmptcmulcn  12852  dveflem  12855  sin0pilem1  12862  sinperlem  12889  ptolemy  12905  tangtx  12919  abssinper  12927  trilpolemeq1  13233  trilpolemlt1  13234