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

Theorem oveq2d 5580
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
StepHypRef Expression
1 oveq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 oveq2 5572 . 2  |-  ( A  =  B  ->  ( C F A )  =  ( C F B ) )
31, 2syl 14 1  |-  ( ph  ->  ( C F A )  =  ( C F B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285  (class class class)co 5564
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359  df-v 2612  df-un 2986  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-br 3806  df-iota 4917  df-fv 4960  df-ov 5567
This theorem is referenced by:  csbov1g  5597  caovassg  5711  caovdig  5727  caovdirg  5730  caov32d  5733  caov4d  5737  caov42d  5739  grprinvlem  5747  grprinvd  5748  grpridd  5749  nnaass  6150  nndi  6151  nnmass  6152  nnmsucr  6153  ecovass  6303  ecoviass  6304  ecovdi  6305  ecovidi  6306  addasspig  6652  mulasspig  6654  distrpig  6655  dfplpq2  6676  mulpipq2  6693  addassnqg  6704  prarloclemarch  6740  prarloclemarch2  6741  ltrnqg  6742  enq0sym  6754  addnq0mo  6769  mulnq0mo  6770  addnnnq0  6771  nq0a0  6779  distrnq0  6781  addassnq0  6784  prarloclemlo  6816  prarloclem3  6819  prarloclem5  6822  prarloclemcalc  6824  addnqprl  6851  addnqpru  6852  prmuloclemcalc  6887  mulnqprl  6890  mulnqpru  6891  distrlem4prl  6906  distrlem4pru  6907  1idprl  6912  1idpru  6913  ltexprlemloc  6929  addcanprleml  6936  addcanprlemu  6937  recexprlem1ssu  6956  ltmprr  6964  caucvgprlemcanl  6966  cauappcvgprlemladdru  6978  cauappcvgprlemladdrl  6979  cauappcvgprlem1  6981  cauappcvgprlemlim  6983  caucvgprlemnkj  6988  caucvgprlemnbj  6989  caucvgprlemdisj  6996  caucvgprlemloc  6997  caucvgprlemcl  6998  caucvgprlemladdrl  7000  caucvgprlem1  7001  caucvgpr  7004  caucvgprprlemell  7007  caucvgprprlemcbv  7009  caucvgprprlemval  7010  caucvgprprlemnkeqj  7012  caucvgprprlemopl  7019  caucvgprprlemlol  7020  caucvgprprlemloc  7025  caucvgprprlemclphr  7027  caucvgprprlemexb  7029  caucvgprprlemaddq  7030  caucvgprprlem1  7031  addcmpblnr  7048  mulcmpblnrlemg  7049  addsrmo  7052  mulsrmo  7053  addsrpr  7054  mulsrpr  7055  ltsrprg  7056  recexgt0sr  7082  mulgt0sr  7086  caucvgsrlemgt1  7103  caucvgsrlemoffval  7104  caucvgsr  7110  mulcnsr  7135  pitoregt0  7149  recidpirqlemcalc  7157  axmulcom  7169  axmulass  7171  axdistr  7172  ax0id  7176  axcnre  7179  recriota  7188  axcaucvglemcau  7196  axcaucvglemres  7197  mulid1  7248  adddirp1d  7277  mul32  7375  mul31  7376  add32  7404  add4  7406  add42  7407  cnegex  7423  addcan2  7426  addsubass  7455  subsub2  7473  nppcan2  7476  sub32  7479  nnncan  7480  sub4  7490  muladd  7625  subdi  7626  mul2neg  7639  submul2  7640  mulsub  7642  mulsubfacd  7659  add20  7715  recexre  7815  rereim  7823  apreap  7824  ltmul1  7829  cru  7839  apreim  7840  mulreim  7841  apadd1  7845  apneg  7848  mulap0  7881  divrecap  7913  divassap  7915  divmulasscomap  7921  divsubdirap  7933  divdivdivap  7938  divmul24ap  7941  divmuleqap  7942  divcanap6  7944  divdivap1  7948  divdivap2  7949  divsubdivap  7953  conjmulap  7954  div2negap  7960  apmul1  8013  cju  8175  nnmulcl  8197  add1p1  8417  sub1m1  8418  cnm2m1cnm3  8419  xp1d2m1eqxm1d2  8420  div4p1lem1div2  8421  un0addcl  8458  un0mulcl  8459  zaddcllemneg  8541  qapne  8875  cnref1o  8884  lincmb01cmp  9171  iccf1o  9172  ige3m2fz  9214  fztp  9241  fzsuc2  9242  fseq1m1p1  9258  fzm1  9263  ige2m1fz1  9272  nn0split  9294  fzval3  9360  zpnn0elfzo1  9364  fzosplitsnm1  9365  fzosplitprm1  9390  fzoshftral  9394  rebtwn2zlemstep  9409  flhalf  9454  modqval  9476  modqvalr  9477  modqdiffl  9487  modqfrac  9489  flqmod  9490  intqfrac  9491  zmod10  9492  modqmulnn  9494  modqvalp1  9495  modqid  9501  modqcyc  9511  modqcyc2  9512  modqmul1  9529  q2submod  9537  modqdi  9544  modqsubdir  9545  modqeqmodmin  9546  modsumfzodifsn  9548  addmodlteq  9550  frecuzrdgsuctlem  9575  uzsinds  9588  iseqeq3  9596  iseqval  9600  iseqvalcbv  9601  iseqvalt  9602  iseqfclt  9606  iseqp1  9608  iseqp1t  9609  iseqm1  9613  iseqfveq2  9614  iseqshft2  9618  monoord2  9622  isermono  9623  iseqsplit  9624  iseqcaopr3  9626  iseqcaopr2  9627  iseqcaopr  9628  iseqid2  9634  iseqhomo  9635  iseqz  9636  expivallem  9644  expival  9645  expp1  9650  expnegap0  9651  expineg2  9652  expn1ap0  9653  expm1t  9671  1exp  9672  expnegzap  9677  mulexpzap  9683  expadd  9685  expaddzaplem  9686  expaddzap  9687  expmul  9688  expmulzap  9689  m1expeven  9690  expsubap  9691  expp1zap  9692  expm1ap  9693  expdivap  9694  iexpcyc  9746  subsq2  9749  binom2  9752  binom21  9753  binom2sub  9754  mulbinom2  9756  binom3  9757  zesq  9758  bernneq  9760  sqoddm1div8  9792  nn0opthlem1d  9814  nn0opthd  9816  facp1  9824  facnn2  9828  faclbnd  9835  faclbnd6  9838  bcval  9843  bccmpl  9848  bcn0  9849  bcnn  9851  bcnp1n  9853  bcm1k  9854  bcp1n  9855  bcp1nk  9856  ibcval5  9857  bcp1m1  9859  bcpasc  9860  bcn2m1  9863  bcn2p1  9864  omgadd  9896  hashunlem  9898  hashunsng  9901  hashdifsn  9913  hashxp  9920  shftcan1  9941  shftcan2  9942  cjval  9951  cjth  9952  crre  9963  replim  9965  remim  9966  reim0b  9968  rereb  9969  mulreap  9970  cjreb  9972  recj  9973  reneg  9974  readd  9975  resub  9976  remullem  9977  imcj  9981  imneg  9982  imadd  9983  imsub  9984  cjcj  9989  cjadd  9990  ipcnval  9992  cjmulrcl  9993  cjneg  9996  addcj  9997  cjsub  9998  cnrecnv  10016  caucvgrelemcau  10085  cvg1nlemcau  10089  cvg1nlemres  10090  recvguniqlem  10099  resqrexlemover  10115  resqrexlemlo  10118  resqrexlemcalc1  10119  resqrexlemcalc3  10121  resqrexlemnm  10123  resqrexlemcvg  10124  absneg  10155  abscj  10157  sqabsadd  10160  sqabssub  10161  absmul  10174  absid  10176  absre  10182  absresq  10183  absexpzap  10185  recvalap  10202  abstri  10209  abs2dif2  10212  recan  10214  cau3lem  10219  amgm2  10223  climaddc1  10386  climsubc1  10389  climcvg1nlem  10405  serif0  10408  dvdsexp  10487  oexpneg  10502  opeo  10522  omeo  10523  m1exp1  10526  flodddiv4  10559  flodddiv4t2lthalf  10562  divgcdnnr  10592  gcdaddm  10600  gcdadd  10601  gcdid  10602  modgcd  10607  bezoutlemnewy  10610  bezoutlema  10613  bezoutlemb  10614  bezoutlemex  10615  bezoutlembz  10618  absmulgcd  10631  gcdmultiple  10634  gcdmultiplez  10635  rpmulgcd  10640  rplpwr  10641  eucalginv  10663  eucialg  10666  lcmneg  10681  lcmgcdlem  10684  lcmgcd  10685  lcmid  10687  lcm1  10688  mulgcddvds  10701  qredeq  10703  divgcdcoprmex  10709  prmind2  10727  rpexp1i  10758  pw2dvdslemn  10768  pw2dvdseulemle  10770  pw2dvdseu  10771  oddpwdclemxy  10772  oddpwdclemdvds  10773  oddpwdclemndvds  10774  oddpwdclemdc  10776  2sqpwodd  10779  nn0gcdsq  10803  phiprmpw  10823  hashgcdlem  10828  qdencn  11070
  Copyright terms: Public domain W3C validator