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

Theorem oveq2d 5756
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 5748 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  (class class class)co 5740
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rex 2397  df-v 2660  df-un 3043  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-iota 5056  df-fv 5099  df-ov 5743
This theorem is referenced by:  csbov1g  5777  caovassg  5895  caovdig  5911  caovdirg  5914  caov32d  5917  caov4d  5921  caov42d  5923  grprinvlem  5931  grprinvd  5932  grpridd  5933  nnaass  6347  nndi  6348  nnmass  6349  nnmsucr  6350  ecovass  6504  ecoviass  6505  ecovdi  6506  ecovidi  6507  addasspig  7102  mulasspig  7104  distrpig  7105  dfplpq2  7126  mulpipq2  7143  addassnqg  7154  prarloclemarch  7190  prarloclemarch2  7191  ltrnqg  7192  enq0sym  7204  addnq0mo  7219  mulnq0mo  7220  addnnnq0  7221  nq0a0  7229  distrnq0  7231  addassnq0  7234  prarloclemlo  7266  prarloclem3  7269  prarloclem5  7272  prarloclemcalc  7274  addnqprl  7301  addnqpru  7302  prmuloclemcalc  7337  mulnqprl  7340  mulnqpru  7341  distrlem4prl  7356  distrlem4pru  7357  1idprl  7362  1idpru  7363  ltexprlemloc  7379  addcanprleml  7386  addcanprlemu  7387  recexprlem1ssu  7406  ltmprr  7414  caucvgprlemcanl  7416  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  cauappcvgprlem1  7431  cauappcvgprlemlim  7433  caucvgprlemnkj  7438  caucvgprlemnbj  7439  caucvgprlemdisj  7446  caucvgprlemloc  7447  caucvgprlemcl  7448  caucvgprlemladdrl  7450  caucvgprlem1  7451  caucvgpr  7454  caucvgprprlemell  7457  caucvgprprlemcbv  7459  caucvgprprlemval  7460  caucvgprprlemnkeqj  7462  caucvgprprlemopl  7469  caucvgprprlemlol  7470  caucvgprprlemloc  7475  caucvgprprlemclphr  7477  caucvgprprlemexb  7479  caucvgprprlemaddq  7480  caucvgprprlem1  7481  addcmpblnr  7511  mulcmpblnrlemg  7512  addsrmo  7515  mulsrmo  7516  addsrpr  7517  mulsrpr  7518  ltsrprg  7519  recexgt0sr  7545  mulgt0sr  7550  caucvgsrlemgt1  7567  caucvgsrlemoffval  7568  caucvgsr  7574  suplocsrlemb  7578  suplocsrlempr  7579  suplocsrlem  7580  suplocsr  7581  mulcnsr  7607  pitoregt0  7621  recidpirqlemcalc  7629  axmulcom  7643  axmulass  7645  axdistr  7646  ax0id  7650  axcnre  7653  recriota  7662  axcaucvglemcau  7670  axcaucvglemres  7671  mulid1  7727  adddirp1d  7756  mul32  7856  mul31  7857  add32  7885  add4  7887  add42  7888  cnegex  7904  addcan2  7907  addsubass  7936  subsub2  7954  nppcan2  7957  sub32  7960  nnncan  7961  sub4  7971  muladd  8110  subdi  8111  mul2neg  8124  submul2  8125  mulsub  8127  mulsubfacd  8144  add20  8200  recexre  8303  rereim  8311  apreap  8312  ltmul1  8317  cru  8327  apreim  8328  mulreim  8329  apadd1  8333  apneg  8336  mulap0  8378  divrecap  8411  divassap  8413  divmulasscomap  8419  divsubdirap  8431  divdivdivap  8436  divmul24ap  8439  divmuleqap  8440  divcanap6  8442  divdivap1  8446  divdivap2  8447  divsubdivap  8451  conjmulap  8452  div2negap  8458  apmul1  8511  cju  8679  nnmulcl  8701  add1p1  8923  sub1m1  8924  cnm2m1cnm3  8925  xp1d2m1eqxm1d2  8926  div4p1lem1div2  8927  un0addcl  8964  un0mulcl  8965  zaddcllemneg  9047  qapne  9383  cnref1o  9392  rexsub  9587  xnegid  9593  xaddcom  9595  xnegdi  9602  xaddass  9603  xaddass2  9604  xpncan  9605  xnpcan  9606  xleadd1a  9607  xsubge0  9615  xposdif  9616  xlesubadd  9617  xadd4d  9619  lincmb01cmp  9737  iccf1o  9738  ige3m2fz  9780  fztp  9809  fzsuc2  9810  fseq1m1p1  9826  fzm1  9831  ige2m1fz1  9840  nn0split  9864  nnsplit  9865  fzval3  9932  zpnn0elfzo1  9936  fzosplitsnm1  9937  fzosplitprm1  9962  fzoshftral  9966  rebtwn2zlemstep  9981  flhalf  10026  modqval  10048  modqvalr  10049  modqdiffl  10059  modqfrac  10061  flqmod  10062  intqfrac  10063  zmod10  10064  modqmulnn  10066  modqvalp1  10067  modqid  10073  modqcyc  10083  modqcyc2  10084  modqmul1  10101  q2submod  10109  modqdi  10116  modqsubdir  10117  modqeqmodmin  10118  modsumfzodifsn  10120  addmodlteq  10122  frecuzrdgsuctlem  10147  uzsinds  10166  seqeq3  10174  iseqvalcbv  10181  seq3val  10182  seqvalcd  10183  seqf  10185  seq3p1  10186  seqovcd  10187  seqp1cd  10190  seq3m1  10192  seq3fveq2  10193  seq3shft2  10197  monoord2  10201  ser3mono  10202  seq3split  10203  seq3caopr3  10205  seq3caopr2  10206  seq3caopr  10207  seq3id2  10233  seq3homo  10234  seq3z  10235  exp3vallem  10245  exp3val  10246  expp1  10251  expnegap0  10252  expineg2  10253  expn1ap0  10254  expm1t  10272  1exp  10273  expnegzap  10278  mulexpzap  10284  expadd  10286  expaddzaplem  10287  expaddzap  10288  expmul  10289  expmulzap  10290  m1expeven  10291  expsubap  10292  expp1zap  10293  expm1ap  10294  expdivap  10295  iexpcyc  10348  subsq2  10351  binom2  10354  binom21  10355  binom2sub  10356  binom2sub1  10357  mulbinom2  10359  binom3  10360  zesq  10361  bernneq  10363  sqoddm1div8  10395  nn0opthlem1d  10417  nn0opthd  10419  facp1  10427  facnn2  10431  faclbnd  10438  faclbnd6  10441  bcval  10446  bccmpl  10451  bcn0  10452  bcnn  10454  bcnp1n  10456  bcm1k  10457  bcp1n  10458  bcp1nk  10459  bcval5  10460  bcp1m1  10462  bcpasc  10463  bcn2m1  10466  bcn2p1  10467  omgadd  10499  hashunlem  10501  hashunsng  10504  hashdifsn  10516  hashxp  10523  zfz1isolemsplit  10532  zfz1isolem1  10534  zfz1iso  10535  seq3coll  10536  shftcan1  10557  shftcan2  10558  cjval  10568  cjth  10569  crre  10580  replim  10582  remim  10583  reim0b  10585  rereb  10586  mulreap  10587  cjreb  10589  recj  10590  reneg  10591  readd  10592  resub  10593  remullem  10594  imcj  10598  imneg  10599  imadd  10600  imsub  10601  cjcj  10606  cjadd  10607  ipcnval  10609  cjmulrcl  10610  cjneg  10613  addcj  10614  cjsub  10615  cnrecnv  10633  caucvgrelemcau  10703  cvg1nlemcau  10707  cvg1nlemres  10708  recvguniqlem  10717  resqrexlemover  10733  resqrexlemlo  10736  resqrexlemcalc1  10737  resqrexlemcalc3  10739  resqrexlemnm  10741  resqrexlemcvg  10742  absneg  10773  abscj  10775  sqabsadd  10778  sqabssub  10779  absmul  10792  absid  10794  absre  10800  absresq  10801  absexpzap  10803  recvalap  10820  abstri  10827  abs2dif2  10830  recan  10832  cau3lem  10837  amgm2  10841  bdtrilem  10961  xrmaxadd  10981  xrbdtri  10996  climaddc1  11049  climsubc1  11052  climcvg1nlem  11069  serf0  11072  summodclem3  11100  summodclem2a  11101  summodc  11103  fsumsplitsn  11130  fsumm1  11136  fsumsplitsnun  11139  fsump1  11140  isummulc2  11146  fsumrev  11163  fisum0diag2  11167  fsummulc2  11168  fsumsub  11172  fsumabs  11185  telfsumo  11186  fsumparts  11190  fsumrelem  11191  fsumiun  11197  binomlem  11203  binom  11204  binom1p  11205  binom11  11206  binom1dif  11207  bcxmas  11209  isumsplit  11211  isum1p  11212  divcnv  11217  arisum2  11219  trireciplem  11220  trirecip  11221  geolim  11231  georeclim  11233  geo2sum  11234  geo2lim  11236  geoisum1c  11240  0.999...  11241  cvgratnnlemnexp  11244  cvgratnnlemmn  11245  cvgratz  11252  mertenslem2  11256  mertensabs  11257  ege2le3  11287  efaddlem  11290  efsub  11297  efexp  11298  eftlub  11306  efsep  11307  effsumlt  11308  ef4p  11310  tanval3ap  11331  resinval  11332  recosval  11333  efi4p  11334  efival  11349  efmival  11350  efeul  11351  sinadd  11353  cosadd  11354  tanaddap  11356  sinsub  11357  cossub  11358  sincossq  11365  sin2t  11366  cos2t  11367  cos2tsin  11368  ef01bndlem  11373  sin01bnd  11374  cos01bnd  11375  absef  11385  absefib  11386  efieq1re  11387  demoivreALT  11389  eirraplem  11390  dvdsexp  11466  oexpneg  11481  opeo  11501  omeo  11502  m1exp1  11505  flodddiv4  11538  flodddiv4t2lthalf  11541  divgcdnnr  11571  gcdaddm  11579  gcdadd  11580  gcdid  11581  modgcd  11586  gcdmultipled  11588  dvdsgcdidd  11589  bezoutlemnewy  11591  bezoutlema  11594  bezoutlemb  11595  bezoutlemex  11596  bezoutlembz  11599  absmulgcd  11612  gcdmultiple  11615  gcdmultiplez  11616  rpmulgcd  11621  rplpwr  11622  eucalginv  11644  eucalg  11647  lcmneg  11662  lcmgcdlem  11665  lcmgcd  11666  lcmid  11668  lcm1  11669  mulgcddvds  11682  qredeq  11684  divgcdcoprmex  11690  prmind2  11708  rpexp1i  11739  pw2dvdslemn  11749  pw2dvdseulemle  11751  pw2dvdseu  11752  oddpwdclemxy  11753  oddpwdclemdvds  11754  oddpwdclemndvds  11755  oddpwdclemdc  11757  2sqpwodd  11760  nn0gcdsq  11784  phiprmpw  11804  hashgcdlem  11809  restabs  12250  cnprcl2k  12281  cnrest2r  12312  ispsmet  12398  psmettri2  12403  psmetsym  12404  ismet  12419  isxmet  12420  xmettri2  12436  xmetsym  12443  xmettri3  12449  mettri3  12450  xblss2ps  12479  xblss2  12480  comet  12574  xmetxp  12582  xmetxpbl  12583  txmetcnp  12593  fsumcncntop  12631  cncfi  12640  limccl  12703  ellimc3apf  12704  limccnpcntop  12719  limccnp2lem  12720  reldvg  12723  dvfvalap  12725  eldvap  12726  dvcj  12748  dvfre  12749  dvexp  12750  dvexp2  12751  dvrecap  12752  dvmptaddx  12756  dvmptmulx  12757  dvmptnegcn  12759  dvmptsubcn  12760  dveflem  12761  dvef  12762  qdencn  13056  trilpolemclim  13063  trilpolemcl  13064  trilpolemisumle  13065  trilpolemeq1  13067  trilpolemlt1  13068  trilpo  13070
  Copyright terms: Public domain W3C validator