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

Theorem oveq2d 5758
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 5750 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316  (class class class)co 5742
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-iota 5058  df-fv 5101  df-ov 5745
This theorem is referenced by:  csbov1g  5779  caovassg  5897  caovdig  5913  caovdirg  5916  caov32d  5919  caov4d  5923  caov42d  5925  grprinvlem  5933  grprinvd  5934  grpridd  5935  nnaass  6349  nndi  6350  nnmass  6351  nnmsucr  6352  ecovass  6506  ecoviass  6507  ecovdi  6508  ecovidi  6509  addasspig  7106  mulasspig  7108  distrpig  7109  dfplpq2  7130  mulpipq2  7147  addassnqg  7158  prarloclemarch  7194  prarloclemarch2  7195  ltrnqg  7196  enq0sym  7208  addnq0mo  7223  mulnq0mo  7224  addnnnq0  7225  nq0a0  7233  distrnq0  7235  addassnq0  7238  prarloclemlo  7270  prarloclem3  7273  prarloclem5  7276  prarloclemcalc  7278  addnqprl  7305  addnqpru  7306  prmuloclemcalc  7341  mulnqprl  7344  mulnqpru  7345  distrlem4prl  7360  distrlem4pru  7361  1idprl  7366  1idpru  7367  ltexprlemloc  7383  addcanprleml  7390  addcanprlemu  7391  recexprlem1ssu  7410  ltmprr  7418  caucvgprlemcanl  7420  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem1  7435  cauappcvgprlemlim  7437  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemcl  7452  caucvgprlemladdrl  7454  caucvgprlem1  7455  caucvgpr  7458  caucvgprprlemell  7461  caucvgprprlemcbv  7463  caucvgprprlemval  7464  caucvgprprlemnkeqj  7466  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemloc  7479  caucvgprprlemclphr  7481  caucvgprprlemexb  7483  caucvgprprlemaddq  7484  caucvgprprlem1  7485  addcmpblnr  7515  mulcmpblnrlemg  7516  addsrmo  7519  mulsrmo  7520  addsrpr  7521  mulsrpr  7522  ltsrprg  7523  recexgt0sr  7549  mulgt0sr  7554  caucvgsrlemgt1  7571  caucvgsrlemoffval  7572  caucvgsr  7578  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  suplocsr  7585  mulcnsr  7611  pitoregt0  7625  recidpirqlemcalc  7633  axmulcom  7647  axmulass  7649  axdistr  7650  ax0id  7654  axcnre  7657  recriota  7666  axcaucvglemcau  7674  axcaucvglemres  7675  mulid1  7731  adddirp1d  7760  mul32  7860  mul31  7861  add32  7889  add4  7891  add42  7892  cnegex  7908  addcan2  7911  addsubass  7940  subsub2  7958  nppcan2  7961  sub32  7964  nnncan  7965  sub4  7975  muladd  8114  subdi  8115  mul2neg  8128  submul2  8129  mulsub  8131  mulsubfacd  8148  add20  8204  recexre  8307  rereim  8315  apreap  8316  ltmul1  8321  cru  8331  apreim  8332  mulreim  8333  apadd1  8337  apneg  8340  mulap0  8382  divrecap  8415  divassap  8417  divmulasscomap  8423  divsubdirap  8435  divdivdivap  8440  divmul24ap  8443  divmuleqap  8444  divcanap6  8446  divdivap1  8450  divdivap2  8451  divsubdivap  8455  conjmulap  8456  div2negap  8462  apmul1  8515  cju  8683  nnmulcl  8705  add1p1  8927  sub1m1  8928  cnm2m1cnm3  8929  xp1d2m1eqxm1d2  8930  div4p1lem1div2  8931  un0addcl  8968  un0mulcl  8969  zaddcllemneg  9051  qapne  9387  cnref1o  9396  rexsub  9591  xnegid  9597  xaddcom  9599  xnegdi  9606  xaddass  9607  xaddass2  9608  xpncan  9609  xnpcan  9610  xleadd1a  9611  xsubge0  9619  xposdif  9620  xlesubadd  9621  xadd4d  9623  lincmb01cmp  9741  iccf1o  9742  ige3m2fz  9784  fztp  9813  fzsuc2  9814  fseq1m1p1  9830  fzm1  9835  ige2m1fz1  9844  nn0split  9868  nnsplit  9869  fzval3  9936  zpnn0elfzo1  9940  fzosplitsnm1  9941  fzosplitprm1  9966  fzoshftral  9970  rebtwn2zlemstep  9985  flhalf  10030  modqval  10052  modqvalr  10053  modqdiffl  10063  modqfrac  10065  flqmod  10066  intqfrac  10067  zmod10  10068  modqmulnn  10070  modqvalp1  10071  modqid  10077  modqcyc  10087  modqcyc2  10088  modqmul1  10105  q2submod  10113  modqdi  10120  modqsubdir  10121  modqeqmodmin  10122  modsumfzodifsn  10124  addmodlteq  10126  frecuzrdgsuctlem  10151  uzsinds  10170  seqeq3  10178  iseqvalcbv  10185  seq3val  10186  seqvalcd  10187  seqf  10189  seq3p1  10190  seqovcd  10191  seqp1cd  10194  seq3m1  10196  seq3fveq2  10197  seq3shft2  10201  monoord2  10205  ser3mono  10206  seq3split  10207  seq3caopr3  10209  seq3caopr2  10210  seq3caopr  10211  seq3id2  10237  seq3homo  10238  seq3z  10239  exp3vallem  10249  exp3val  10250  expp1  10255  expnegap0  10256  expineg2  10257  expn1ap0  10258  expm1t  10276  1exp  10277  expnegzap  10282  mulexpzap  10288  expadd  10290  expaddzaplem  10291  expaddzap  10292  expmul  10293  expmulzap  10294  m1expeven  10295  expsubap  10296  expp1zap  10297  expm1ap  10298  expdivap  10299  iexpcyc  10352  subsq2  10355  binom2  10358  binom21  10359  binom2sub  10360  binom2sub1  10361  mulbinom2  10363  binom3  10364  zesq  10365  bernneq  10367  sqoddm1div8  10399  nn0opthlem1d  10421  nn0opthd  10423  facp1  10431  facnn2  10435  faclbnd  10442  faclbnd6  10445  bcval  10450  bccmpl  10455  bcn0  10456  bcnn  10458  bcnp1n  10460  bcm1k  10461  bcp1n  10462  bcp1nk  10463  bcval5  10464  bcp1m1  10466  bcpasc  10467  bcn2m1  10470  bcn2p1  10471  omgadd  10503  hashunlem  10505  hashunsng  10508  hashdifsn  10520  hashxp  10527  zfz1isolemsplit  10536  zfz1isolem1  10538  zfz1iso  10539  seq3coll  10540  shftcan1  10561  shftcan2  10562  cjval  10572  cjth  10573  crre  10584  replim  10586  remim  10587  reim0b  10589  rereb  10590  mulreap  10591  cjreb  10593  recj  10594  reneg  10595  readd  10596  resub  10597  remullem  10598  imcj  10602  imneg  10603  imadd  10604  imsub  10605  cjcj  10610  cjadd  10611  ipcnval  10613  cjmulrcl  10614  cjneg  10617  addcj  10618  cjsub  10619  cnrecnv  10637  caucvgrelemcau  10707  cvg1nlemcau  10711  cvg1nlemres  10712  recvguniqlem  10721  resqrexlemover  10737  resqrexlemlo  10740  resqrexlemcalc1  10741  resqrexlemcalc3  10743  resqrexlemnm  10745  resqrexlemcvg  10746  absneg  10777  abscj  10779  sqabsadd  10782  sqabssub  10783  absmul  10796  absid  10798  absre  10804  absresq  10805  absexpzap  10807  recvalap  10824  abstri  10831  abs2dif2  10834  recan  10836  cau3lem  10841  amgm2  10845  bdtrilem  10965  xrmaxadd  10985  xrbdtri  11000  climaddc1  11053  climsubc1  11056  climcvg1nlem  11073  serf0  11076  summodclem3  11104  summodclem2a  11105  summodc  11107  fsumsplitsn  11134  fsumm1  11140  fsumsplitsnun  11143  fsump1  11144  isummulc2  11150  fsumrev  11167  fisum0diag2  11171  fsummulc2  11172  fsumsub  11176  fsumabs  11189  telfsumo  11190  fsumparts  11194  fsumrelem  11195  fsumiun  11201  binomlem  11207  binom  11208  binom1p  11209  binom11  11210  binom1dif  11211  bcxmas  11213  isumsplit  11215  isum1p  11216  divcnv  11221  arisum2  11223  trireciplem  11224  trirecip  11225  geolim  11235  georeclim  11237  geo2sum  11238  geo2lim  11240  geoisum1c  11244  0.999...  11245  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  cvgratz  11256  mertenslem2  11260  mertensabs  11261  ege2le3  11291  efaddlem  11294  efsub  11301  efexp  11302  eftlub  11310  efsep  11311  effsumlt  11312  ef4p  11314  tanval3ap  11335  resinval  11336  recosval  11337  efi4p  11338  efival  11353  efmival  11354  efeul  11355  sinadd  11357  cosadd  11358  tanaddap  11360  sinsub  11361  cossub  11362  sincossq  11369  sin2t  11370  cos2t  11371  cos2tsin  11372  ef01bndlem  11377  sin01bnd  11378  cos01bnd  11379  cos12dec  11388  absef  11390  absefib  11391  efieq1re  11392  demoivreALT  11394  eirraplem  11395  dvdsexp  11471  oexpneg  11486  opeo  11506  omeo  11507  m1exp1  11510  flodddiv4  11543  flodddiv4t2lthalf  11546  divgcdnnr  11576  gcdaddm  11584  gcdadd  11585  gcdid  11586  modgcd  11591  gcdmultipled  11593  dvdsgcdidd  11594  bezoutlemnewy  11596  bezoutlema  11599  bezoutlemb  11600  bezoutlemex  11601  bezoutlembz  11604  absmulgcd  11617  gcdmultiple  11620  gcdmultiplez  11621  rpmulgcd  11626  rplpwr  11627  eucalginv  11649  eucalg  11652  lcmneg  11667  lcmgcdlem  11670  lcmgcd  11671  lcmid  11673  lcm1  11674  mulgcddvds  11687  qredeq  11689  divgcdcoprmex  11695  prmind2  11713  rpexp1i  11744  pw2dvdslemn  11754  pw2dvdseulemle  11756  pw2dvdseu  11757  oddpwdclemxy  11758  oddpwdclemdvds  11759  oddpwdclemndvds  11760  oddpwdclemdc  11762  2sqpwodd  11765  nn0gcdsq  11789  phiprmpw  11809  hashgcdlem  11814  restabs  12255  cnprcl2k  12286  cnrest2r  12317  ispsmet  12403  psmettri2  12408  psmetsym  12409  ismet  12424  isxmet  12425  xmettri2  12441  xmetsym  12448  xmettri3  12454  mettri3  12455  xblss2ps  12484  xblss2  12485  comet  12579  xmetxp  12587  xmetxpbl  12588  txmetcnp  12598  fsumcncntop  12636  cncfi  12645  limccl  12708  ellimc3apf  12709  limccnpcntop  12724  limccnp2lem  12725  reldvg  12728  dvfvalap  12730  eldvap  12731  dvcj  12753  dvfre  12754  dvexp  12755  dvexp2  12756  dvrecap  12757  dvmptaddx  12761  dvmptmulx  12762  dvmptnegcn  12764  dvmptsubcn  12765  dveflem  12766  dvef  12767  sin0pilem1  12773  sin0pilem2  12774  efper  12799  sinperlem  12800  efimpi  12811  ptolemy  12816  qdencn  13118  trilpolemclim  13125  trilpolemcl  13126  trilpolemisumle  13127  trilpolemeq1  13129  trilpolemlt1  13130  trilpo  13132
  Copyright terms: Public domain W3C validator