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

Theorem oveq2d 5506
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 5498 . 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 1243  (class class class)co 5490
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2309  df-v 2556  df-un 2919  df-sn 3378  df-pr 3379  df-op 3381  df-uni 3578  df-br 3762  df-iota 4845  df-fv 4888  df-ov 5493
This theorem is referenced by:  csbov1g  5523  caovassg  5637  caovdig  5653  caovdirg  5656  caov32d  5659  caov4d  5663  caov42d  5665  grprinvlem  5673  grprinvd  5674  grpridd  5675  nnaass  6042  nndi  6043  nnmass  6044  nnmsucr  6045  ecovass  6193  ecoviass  6194  ecovdi  6195  ecovidi  6196  addasspig  6400  mulasspig  6402  distrpig  6403  dfplpq2  6424  mulpipq2  6441  addassnqg  6452  prarloclemarch  6488  prarloclemarch2  6489  ltrnqg  6490  enq0sym  6502  addnq0mo  6517  mulnq0mo  6518  addnnnq0  6519  nq0a0  6527  distrnq0  6529  addassnq0  6532  prarloclemlo  6564  prarloclem3  6567  prarloclem5  6570  prarloclemcalc  6572  addnqprl  6599  addnqpru  6600  prmuloclemcalc  6635  mulnqprl  6638  mulnqpru  6639  distrlem4prl  6654  distrlem4pru  6655  1idprl  6660  1idpru  6661  ltexprlemloc  6677  addcanprleml  6684  addcanprlemu  6685  recexprlem1ssu  6704  ltmprr  6712  caucvgprlemcanl  6714  cauappcvgprlemladdru  6726  cauappcvgprlemladdrl  6727  cauappcvgprlem1  6729  cauappcvgprlemlim  6731  caucvgprlemnkj  6736  caucvgprlemnbj  6737  caucvgprlemdisj  6744  caucvgprlemloc  6745  caucvgprlemcl  6746  caucvgprlemladdrl  6748  caucvgprlem1  6749  caucvgpr  6752  caucvgprprlemell  6755  caucvgprprlemcbv  6757  caucvgprprlemval  6758  caucvgprprlemnkeqj  6760  caucvgprprlemopl  6767  caucvgprprlemlol  6768  caucvgprprlemloc  6773  caucvgprprlemclphr  6775  caucvgprprlemexb  6777  caucvgprprlemaddq  6778  caucvgprprlem1  6779  addcmpblnr  6796  mulcmpblnrlemg  6797  addsrmo  6800  mulsrmo  6801  addsrpr  6802  mulsrpr  6803  ltsrprg  6804  recexgt0sr  6830  mulgt0sr  6834  caucvgsrlemgt1  6851  caucvgsrlemoffval  6852  caucvgsr  6858  mulcnsr  6883  pitoregt0  6897  recidpirqlemcalc  6905  axmulcom  6917  axmulass  6919  axdistr  6920  ax0id  6924  axcnre  6927  recriota  6936  axcaucvglemcau  6944  axcaucvglemres  6945  mulid1  6996  mul32  7114  mul31  7115  add32  7141  add4  7143  add42  7144  cnegex  7160  addcan2  7163  addsubass  7192  subsub2  7209  nppcan2  7212  sub32  7215  nnncan  7216  sub4  7226  muladd  7351  subdi  7352  mul2neg  7365  submul2  7366  mulsub  7368  mulsubfacd  7385  add20  7438  recexre  7536  rereim  7544  apreap  7545  ltmul1  7550  cru  7560  apreim  7561  mulreim  7562  apadd1  7566  apneg  7569  mulap0  7602  divrecap  7634  divassap  7636  divsubdirap  7651  divdivdivap  7656  divmul24ap  7659  divmuleqap  7660  divcanap6  7662  divdivap1  7666  divdivap2  7667  divsubdivap  7671  conjmulap  7672  div2negap  7678  apmul1  7731  cju  7880  nnmulcl  7902  add1p1  8138  sub1m1  8139  cnm2m1cnm3  8140  un0addcl  8178  un0mulcl  8179  zaddcllemneg  8247  qapne  8537  cnref1o  8544  lincmb01cmp  8829  iccf1o  8830  ige3m2fz  8871  fztp  8898  fzsuc2  8899  fseq1m1p1  8915  fzm1  8920  ige2m1fz1  8929  nn0split  8952  fzval3  9018  zpnn0elfzo1  9022  fzosplitsnm1  9023  fzosplitprm1  9048  fzoshftral  9052  iseqeq3  9085  iseqval  9089  iseqp1  9094  iseqm1  9096  iseqfveq2  9097  iseqshft2  9101  monoord2  9105  isermono  9106  iseqsplit  9107  iseqcaopr3  9109  iseqcaopr2  9110  iseqcaopr  9111  iseqhomo  9117  expivallem  9125  expival  9126  expp1  9131  expnegap0  9132  expineg2  9133  expn1ap0  9134  expm1t  9152  1exp  9153  expnegzap  9158  mulexpzap  9164  expadd  9166  expaddzaplem  9167  expaddzap  9168  expmul  9169  expmulzap  9170  expsubap  9171  expp1zap  9172  expm1ap  9173  expdivap  9174  subsq2  9228  binom2  9231  binom21  9232  binom2sub  9233  binom3  9235  zesq  9236  bernneq  9238  shftcan1  9304  shftcan2  9305  cjval  9314  cjth  9315  crre  9326  replim  9328  remim  9329  reim0b  9331  rereb  9332  mulreap  9333  cjreb  9335  recj  9336  reneg  9337  readd  9338  resub  9339  remullem  9340  imcj  9344  imneg  9345  imadd  9346  imsub  9347  cjcj  9352  cjadd  9353  ipcnval  9355  cjmulrcl  9356  cjneg  9359  addcj  9360  cjsub  9361  cnrecnv  9379  caucvgrelemcau  9448  cvg1nlemcau  9452  cvg1nlemres  9453  recvguniqlem  9461  resqrexlemover  9477  resqrexlemlo  9480  resqrexlemcalc1  9481  resqrexlemcalc3  9483  resqrexlemnm  9485  resqrexlemcvg  9486  absneg  9517  abscj  9519  sqabsadd  9522  sqabssub  9523  absmul  9536  absid  9538  absre  9542  absresq  9543  absexpzap  9545  recvalap  9562  abstri  9569  abs2dif2  9572  recan  9574  cau3lem  9579  amgm2  9583  climaddc1  9717  climsubc1  9720  climcvg1nlem  9736  serif0  9739
  Copyright terms: Public domain W3C validator