ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  oveq2d GIF version

Theorem oveq2d 5884
Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
Hypothesis
Ref Expression
oveq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
oveq2d (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Proof of Theorem oveq2d
StepHypRef Expression
1 oveq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 oveq2 5876 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353  (class class class)co 5868
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 5173  df-fv 5219  df-ov 5871
This theorem is referenced by:  csbov1g  5908  caovassg  6026  caovdig  6042  caovdirg  6045  caov32d  6048  caov4d  6052  caov42d  6054  nnaass  6479  nndi  6480  nnmass  6481  nnmsucr  6482  ecovass  6637  ecoviass  6638  ecovdi  6639  ecovidi  6640  addasspig  7307  mulasspig  7309  distrpig  7310  dfplpq2  7331  mulpipq2  7348  addassnqg  7359  prarloclemarch  7395  prarloclemarch2  7396  ltrnqg  7397  enq0sym  7409  addnq0mo  7424  mulnq0mo  7425  addnnnq0  7426  nq0a0  7434  distrnq0  7436  addassnq0  7439  prarloclemlo  7471  prarloclem3  7474  prarloclem5  7477  prarloclemcalc  7479  addnqprl  7506  addnqpru  7507  prmuloclemcalc  7542  mulnqprl  7545  mulnqpru  7546  distrlem4prl  7561  distrlem4pru  7562  1idprl  7567  1idpru  7568  ltexprlemloc  7584  addcanprleml  7591  addcanprlemu  7592  recexprlem1ssu  7611  ltmprr  7619  caucvgprlemcanl  7621  cauappcvgprlemladdru  7633  cauappcvgprlemladdrl  7634  cauappcvgprlem1  7636  cauappcvgprlemlim  7638  caucvgprlemnkj  7643  caucvgprlemnbj  7644  caucvgprlemdisj  7651  caucvgprlemloc  7652  caucvgprlemcl  7653  caucvgprlemladdrl  7655  caucvgprlem1  7656  caucvgpr  7659  caucvgprprlemell  7662  caucvgprprlemcbv  7664  caucvgprprlemval  7665  caucvgprprlemnkeqj  7667  caucvgprprlemopl  7674  caucvgprprlemlol  7675  caucvgprprlemloc  7680  caucvgprprlemclphr  7682  caucvgprprlemexb  7684  caucvgprprlemaddq  7685  caucvgprprlem1  7686  addcmpblnr  7716  mulcmpblnrlemg  7717  addsrmo  7720  mulsrmo  7721  addsrpr  7722  mulsrpr  7723  ltsrprg  7724  recexgt0sr  7750  mulgt0sr  7755  caucvgsrlemgt1  7772  caucvgsrlemoffval  7773  caucvgsr  7779  suplocsrlemb  7783  suplocsrlempr  7784  suplocsrlem  7785  suplocsr  7786  mulcnsr  7812  pitoregt0  7826  recidpirqlemcalc  7834  axmulcom  7848  axmulass  7850  axdistr  7851  ax0id  7855  axcnre  7858  recriota  7867  axcaucvglemcau  7875  axcaucvglemres  7876  mulid1  7932  adddirp1d  7961  mul32  8064  mul31  8065  add32  8093  add4  8095  add42  8096  cnegex  8112  addcan2  8115  addsubass  8144  subsub2  8162  nppcan2  8165  sub32  8168  nnncan  8169  sub4  8179  muladd  8318  subdi  8319  mul2neg  8332  submul2  8333  mulsub  8335  mulsubfacd  8352  add20  8408  recexre  8512  rereim  8520  apreap  8521  ltmul1  8526  cru  8536  apreim  8537  mulreim  8538  apadd1  8542  apneg  8545  mulap0  8587  divrecap  8621  divassap  8623  divmulasscomap  8629  divsubdirap  8641  divdivdivap  8646  divmul24ap  8649  divmuleqap  8650  divcanap6  8652  divdivap1  8656  divdivap2  8657  divsubdivap  8661  conjmulap  8662  div2negap  8668  apmul1  8721  cju  8894  nnmulcl  8916  add1p1  9144  sub1m1  9145  cnm2m1cnm3  9146  xp1d2m1eqxm1d2  9147  div4p1lem1div2  9148  un0addcl  9185  un0mulcl  9186  zaddcllemneg  9268  qapne  9615  cnref1o  9626  rexsub  9827  xnegid  9833  xaddcom  9835  xnegdi  9842  xaddass  9843  xaddass2  9844  xpncan  9845  xnpcan  9846  xleadd1a  9847  xsubge0  9855  xposdif  9856  xlesubadd  9857  xadd4d  9859  lincmb01cmp  9977  iccf1o  9978  ige3m2fz  10022  fztp  10051  fzsuc2  10052  fseq1m1p1  10068  fzm1  10073  ige2m1fz1  10082  nn0split  10109  nnsplit  10110  fzval3  10177  zpnn0elfzo1  10181  fzosplitsnm1  10182  fzosplitprm1  10207  fzoshftral  10211  rebtwn2zlemstep  10226  flhalf  10275  modqval  10297  modqvalr  10298  modqdiffl  10308  modqfrac  10310  flqmod  10311  intqfrac  10312  zmod10  10313  modqmulnn  10315  modqvalp1  10316  modqid  10322  modqcyc  10332  modqcyc2  10333  modqmul1  10350  q2submod  10358  modqdi  10365  modqsubdir  10366  modqeqmodmin  10367  modsumfzodifsn  10369  addmodlteq  10371  frecuzrdgsuctlem  10396  uzsinds  10415  seqeq3  10423  iseqvalcbv  10430  seq3val  10431  seqvalcd  10432  seqf  10434  seq3p1  10435  seqovcd  10436  seqp1cd  10439  seq3m1  10441  seq3fveq2  10442  seq3shft2  10446  monoord2  10450  ser3mono  10451  seq3split  10452  seq3caopr3  10454  seq3caopr2  10455  seq3caopr  10456  seq3id2  10482  seq3homo  10483  seq3z  10484  exp3vallem  10494  exp3val  10495  expp1  10500  expnegap0  10501  expineg2  10502  expn1ap0  10503  expm1t  10521  1exp  10522  expnegzap  10527  mulexpzap  10533  expadd  10535  expaddzaplem  10536  expaddzap  10537  expmul  10538  expmulzap  10539  m1expeven  10540  expsubap  10541  expp1zap  10542  expm1ap  10543  expdivap  10544  iexpcyc  10597  subsq2  10600  binom2  10604  binom21  10605  binom2sub  10606  binom2sub1  10607  mulbinom2  10609  binom3  10610  zesq  10611  bernneq  10613  sqoddm1div8  10646  nn0opthlem1d  10671  nn0opthd  10673  facp1  10681  facnn2  10685  faclbnd  10692  faclbnd6  10695  bcval  10700  bccmpl  10705  bcn0  10706  bcnn  10708  bcnp1n  10710  bcm1k  10711  bcp1n  10712  bcp1nk  10713  bcval5  10714  bcp1m1  10716  bcpasc  10717  bcn2m1  10720  bcn2p1  10721  omgadd  10753  hashunlem  10755  hashunsng  10758  hashdifsn  10770  hashxp  10777  zfz1isolemsplit  10789  zfz1isolem1  10791  zfz1iso  10792  seq3coll  10793  shftcan1  10814  shftcan2  10815  cjval  10825  cjth  10826  crre  10837  replim  10839  remim  10840  reim0b  10842  rereb  10843  mulreap  10844  cjreb  10846  recj  10847  reneg  10848  readd  10849  resub  10850  remullem  10851  imcj  10855  imneg  10856  imadd  10857  imsub  10858  cjcj  10863  cjadd  10864  ipcnval  10866  cjmulrcl  10867  cjneg  10870  addcj  10871  cjsub  10872  cnrecnv  10890  caucvgrelemcau  10960  cvg1nlemcau  10964  cvg1nlemres  10965  recvguniqlem  10974  resqrexlemover  10990  resqrexlemlo  10993  resqrexlemcalc1  10994  resqrexlemcalc3  10996  resqrexlemnm  10998  resqrexlemcvg  10999  absneg  11030  abscj  11032  sqabsadd  11035  sqabssub  11036  absmul  11049  absid  11051  absre  11057  absresq  11058  absexpzap  11060  recvalap  11077  abstri  11084  abs2dif2  11087  recan  11089  cau3lem  11094  amgm2  11098  bdtrilem  11218  xrmaxadd  11240  xrbdtri  11255  climaddc1  11308  climsubc1  11311  climcvg1nlem  11328  serf0  11331  summodclem3  11359  summodclem2a  11360  summodc  11362  fsumsplitsn  11389  fsumm1  11395  fsumsplitsnun  11398  fsump1  11399  isummulc2  11405  fsumrev  11422  fisum0diag2  11426  fsummulc2  11427  fsumsub  11431  fsumabs  11444  telfsumo  11445  fsumparts  11449  fsumrelem  11450  fsumiun  11456  binomlem  11462  binom  11463  binom1p  11464  binom11  11465  binom1dif  11466  bcxmas  11468  isumsplit  11470  isum1p  11471  divcnv  11476  arisum2  11478  trireciplem  11479  trirecip  11480  geolim  11490  georeclim  11492  geo2sum  11493  geo2lim  11495  geoisum1c  11499  0.999...  11500  cvgratnnlemnexp  11503  cvgratnnlemmn  11504  cvgratz  11511  mertenslem2  11515  mertensabs  11516  clim2prod  11518  prodfrecap  11525  prodfdivap  11526  prodmodclem3  11554  prodmodclem2a  11555  fprodm1  11577  fprodp1  11579  fprodunsn  11583  fprodfac  11594  fprodeq0  11596  fprodconst  11599  fprodrec  11608  fproddivap  11609  fprodsplitsn  11612  ege2le3  11650  efaddlem  11653  efsub  11660  efexp  11661  eftlub  11669  efsep  11670  effsumlt  11671  ef4p  11673  tanval3ap  11693  resinval  11694  recosval  11695  efi4p  11696  efival  11711  efmival  11712  efeul  11713  sinadd  11715  cosadd  11716  tanaddap  11718  sinsub  11719  cossub  11720  sincossq  11727  sin2t  11728  cos2t  11729  cos2tsin  11730  ef01bndlem  11735  sin01bnd  11736  cos01bnd  11737  cos12dec  11746  absef  11748  absefib  11749  efieq1re  11750  demoivreALT  11752  eirraplem  11755  dvdsexp  11837  oexpneg  11852  opeo  11872  omeo  11873  m1exp1  11876  flodddiv4  11909  flodddiv4t2lthalf  11912  divgcdnnr  11947  gcdaddm  11955  gcdadd  11956  gcdid  11957  modgcd  11962  gcdmultipled  11964  dvdsgcdidd  11965  bezoutlemnewy  11967  bezoutlema  11970  bezoutlemb  11971  bezoutlemex  11972  bezoutlembz  11975  absmulgcd  11988  gcdmultiple  11991  gcdmultiplez  11992  rpmulgcd  11997  rplpwr  11998  eucalginv  12026  eucalg  12029  lcmneg  12044  lcmgcdlem  12047  lcmgcd  12048  lcmid  12050  lcm1  12051  mulgcddvds  12064  qredeq  12066  divgcdcoprmex  12072  prmind2  12090  rpexp1i  12124  pw2dvdslemn  12135  pw2dvdseulemle  12137  pw2dvdseu  12138  oddpwdclemxy  12139  oddpwdclemdvds  12140  oddpwdclemndvds  12141  oddpwdclemdc  12143  2sqpwodd  12146  nn0gcdsq  12170  phiprmpw  12192  eulerthlemrprm  12199  eulerthlema  12200  eulerthlemh  12201  eulerthlemth  12202  fermltl  12204  prmdiv  12205  hashgcdlem  12208  odzdvds  12215  vfermltl  12221  modprm0  12224  nnnn0modprm0  12225  modprmn0modprm0  12226  coprimeprodsq  12227  pythagtriplem1  12235  pythagtriplem4  12238  pythagtriplem12  12245  pythagtriplem14  12247  pythagtriplem16  12249  pythagtriplem18  12251  pythagtrip  12253  pcpremul  12263  pceu  12265  pczpre  12267  pcdiv  12272  pcqmul  12273  pcqdiv  12277  pcexp  12279  pczdvds  12283  pczndvds  12285  pczndvds2  12287  pcid  12293  pcneg  12294  pcdvdstr  12296  pcgcd1  12297  pcgcd  12298  pc2dvds  12299  pcaddlem  12308  pcadd  12309  pcmpt  12311  pcmpt2  12312  fldivp1  12316  pcfac  12318  pcbc  12319  expnprm  12321  prmpwdvds  12323  pockthlem  12324  pockthi  12326  4sqlem7  12352  4sqlem9  12354  4sqlem10  12355  4sqlem2  12357  4sqlem3  12358  4sqlem4  12360  mul4sqlem  12361  ressvalsets  12493  strressid  12499  ressval3d  12500  ressinbasd  12502  ressressg  12503  ressabsg  12504  grprinvlem  12683  grprinvd  12684  grpridd  12685  isnsgrp  12691  sgrpass  12693  sgrp1  12695  mnd32g  12707  mnd4g  12709  mndpropd  12720  mhmlin  12735  grprcan  12787  grpsubval  12796  grpinvid2  12802  grpasscan2  12810  grpsubinv  12819  grpinvadd  12824  grpsubid1  12831  grpsubadd0sub  12833  grpsubadd  12834  grpsubsub  12835  grpaddsubass  12836  grppncan  12837  grpnnncan2  12843  grpsubpropd2  12851  mhmlem  12854  mhmid  12855  mhmmnd  12856  ghmgrp  12858  mulgnnp1  12867  mulgaddcomlem  12881  mulgaddcom  12882  mulginvinv  12884  mulgnn0dir  12888  mulgdirlem  12889  mulgp1  12891  mulgneg2  12892  mulgnn0ass  12894  mulgass  12895  mulgmodid  12897  mulgsubdir  12898  ablsub4  12930  abladdsub4  12931  ablsubsub4  12936  ablsub32  12939  ablnnncan  12940  srgass  12967  srgpcomp  12986  srgpcompp  12987  srgpcomppsc  12988  srg1expzeq1  12991  ringpropd  13030  ringrz  13036  rngnegr  13042  ringmneg2  13044  ringsubdi  13046  rngsubdir  13047  ring1  13049  opprring  13061  mulgass3  13066  dvdsrd  13075  unitgrp  13097  invrfvald  13103  restabs  13308  cnprcl2k  13339  cnrest2r  13370  ispsmet  13456  psmettri2  13461  psmetsym  13462  ismet  13477  isxmet  13478  xmettri2  13494  xmetsym  13501  xmettri3  13507  mettri3  13508  xblss2ps  13537  xblss2  13538  comet  13632  xmetxp  13640  xmetxpbl  13641  txmetcnp  13651  fsumcncntop  13689  cncfi  13698  limccl  13761  ellimc3apf  13762  limccnpcntop  13777  limccnp2lem  13778  reldvg  13781  dvfvalap  13783  eldvap  13784  dvcj  13806  dvfre  13807  dvexp  13808  dvexp2  13809  dvrecap  13810  dvmptaddx  13814  dvmptmulx  13815  dvmptnegcn  13817  dvmptsubcn  13818  dvmptcjx  13819  dveflem  13820  dvef  13821  sin0pilem1  13835  sin0pilem2  13836  efper  13861  sinperlem  13862  efimpi  13873  ptolemy  13878  tangtx  13892  abssinper  13900  cosq34lt1  13904  rpcxpef  13948  rpcxpp1  13960  rpcxpneg  13961  rpcxpsub  13962  rpmulcxp  13963  rpdivcxp  13965  cxpmul  13966  rpcxproot  13967  cxpcom  13990  rpabscxpbnd  13992  rplogbval  13996  rplogbreexp  14004  rplogbzexp  14005  rprelogbmulexp  14007  rprelogbdiv  14008  relogbexpap  14009  rplogbcxp  14014  rpcxplogb  14015  logbgcd1irr  14018  logbgcd1irraplemap  14020  binom4  14030  lgslem1  14034  lgsval  14038  lgsfvalg  14039  lgsval2lem  14044  lgsval4  14054  lgsneg  14058  lgsneg1  14059  lgsmod  14060  lgsdir2  14067  lgsdirprm  14068  lgsdilem2  14070  lgsdi  14071  lgsne0  14072  lgssq2  14075  lgsdirnn0  14081  lgsdinn0  14082  2sqlem2  14084  2sqlem3  14086  2sqlem4  14087  2sqlem8  14092  2sqlem9  14093  2sqlem10  14094  qdencn  14398  trilpolemclim  14407  trilpolemcl  14408  trilpolemisumle  14409  trilpolemeq1  14411  trilpolemlt1  14412  trilpo  14414  apdifflemf  14417  apdiff  14419  iswomni0  14422  redcwlpolemeq1  14425  redcwlpo  14426  nconstwlpolem0  14433  nconstwlpolemgt0  14434  nconstwlpo  14436  neapmkv  14438
  Copyright terms: Public domain W3C validator