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

Theorem oveq2d 5528
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 5520 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243  (class class class)co 5512
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 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515
This theorem is referenced by:  csbov1g  5545  caovassg  5659  caovdig  5675  caovdirg  5678  caov32d  5681  caov4d  5685  caov42d  5687  grprinvlem  5695  grprinvd  5696  grpridd  5697  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  addasspig  6426  mulasspig  6428  distrpig  6429  dfplpq2  6450  mulpipq2  6467  addassnqg  6478  prarloclemarch  6514  prarloclemarch2  6515  ltrnqg  6516  enq0sym  6528  addnq0mo  6543  mulnq0mo  6544  addnnnq0  6545  nq0a0  6553  distrnq0  6555  addassnq0  6558  prarloclemlo  6590  prarloclem3  6593  prarloclem5  6596  prarloclemcalc  6598  addnqprl  6625  addnqpru  6626  prmuloclemcalc  6661  mulnqprl  6664  mulnqpru  6665  distrlem4prl  6680  distrlem4pru  6681  1idprl  6686  1idpru  6687  ltexprlemloc  6703  addcanprleml  6710  addcanprlemu  6711  recexprlem1ssu  6730  ltmprr  6738  caucvgprlemcanl  6740  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  cauappcvgprlem1  6755  cauappcvgprlemlim  6757  caucvgprlemnkj  6762  caucvgprlemnbj  6763  caucvgprlemdisj  6770  caucvgprlemloc  6771  caucvgprlemcl  6772  caucvgprlemladdrl  6774  caucvgprlem1  6775  caucvgpr  6778  caucvgprprlemell  6781  caucvgprprlemcbv  6783  caucvgprprlemval  6784  caucvgprprlemnkeqj  6786  caucvgprprlemopl  6793  caucvgprprlemlol  6794  caucvgprprlemloc  6799  caucvgprprlemclphr  6801  caucvgprprlemexb  6803  caucvgprprlemaddq  6804  caucvgprprlem1  6805  addcmpblnr  6822  mulcmpblnrlemg  6823  addsrmo  6826  mulsrmo  6827  addsrpr  6828  mulsrpr  6829  ltsrprg  6830  recexgt0sr  6856  mulgt0sr  6860  caucvgsrlemgt1  6877  caucvgsrlemoffval  6878  caucvgsr  6884  mulcnsr  6909  pitoregt0  6923  recidpirqlemcalc  6931  axmulcom  6943  axmulass  6945  axdistr  6946  ax0id  6950  axcnre  6953  recriota  6962  axcaucvglemcau  6970  axcaucvglemres  6971  mulid1  7022  mul32  7141  mul31  7142  add32  7168  add4  7170  add42  7171  cnegex  7187  addcan2  7190  addsubass  7219  subsub2  7237  nppcan2  7240  sub32  7243  nnncan  7244  sub4  7254  muladd  7379  subdi  7380  mul2neg  7393  submul2  7394  mulsub  7396  mulsubfacd  7413  add20  7467  recexre  7567  rereim  7575  apreap  7576  ltmul1  7581  cru  7591  apreim  7592  mulreim  7593  apadd1  7597  apneg  7600  mulap0  7633  divrecap  7665  divassap  7667  divsubdirap  7682  divdivdivap  7687  divmul24ap  7690  divmuleqap  7691  divcanap6  7693  divdivap1  7697  divdivap2  7698  divsubdivap  7702  conjmulap  7703  div2negap  7709  apmul1  7762  cju  7911  nnmulcl  7933  add1p1  8172  sub1m1  8173  cnm2m1cnm3  8174  div4p1lem1div2  8175  un0addcl  8213  un0mulcl  8214  zaddcllemneg  8282  qapne  8572  cnref1o  8580  lincmb01cmp  8869  iccf1o  8870  ige3m2fz  8911  fztp  8938  fzsuc2  8939  fseq1m1p1  8955  fzm1  8960  ige2m1fz1  8969  nn0split  8992  fzval3  9058  zpnn0elfzo1  9062  fzosplitsnm1  9063  fzosplitprm1  9088  fzoshftral  9092  rebtwn2zlemstep  9105  flhalf  9142  iseqeq3  9190  iseqval  9194  iseqp1  9199  iseqm1  9201  iseqfveq2  9202  iseqshft2  9206  monoord2  9210  isermono  9211  iseqsplit  9212  iseqcaopr3  9214  iseqcaopr2  9215  iseqcaopr  9216  iseqhomo  9222  expivallem  9230  expival  9231  expp1  9236  expnegap0  9237  expineg2  9238  expn1ap0  9239  expm1t  9257  1exp  9258  expnegzap  9263  mulexpzap  9269  expadd  9271  expaddzaplem  9272  expaddzap  9273  expmul  9274  expmulzap  9275  expsubap  9276  expp1zap  9277  expm1ap  9278  expdivap  9279  subsq2  9333  binom2  9336  binom21  9337  binom2sub  9338  binom3  9340  zesq  9341  bernneq  9343  shftcan1  9409  shftcan2  9410  cjval  9419  cjth  9420  crre  9431  replim  9433  remim  9434  reim0b  9436  rereb  9437  mulreap  9438  cjreb  9440  recj  9441  reneg  9442  readd  9443  resub  9444  remullem  9445  imcj  9449  imneg  9450  imadd  9451  imsub  9452  cjcj  9457  cjadd  9458  ipcnval  9460  cjmulrcl  9461  cjneg  9464  addcj  9465  cjsub  9466  cnrecnv  9484  caucvgrelemcau  9553  cvg1nlemcau  9557  cvg1nlemres  9558  recvguniqlem  9566  resqrexlemover  9582  resqrexlemlo  9585  resqrexlemcalc1  9586  resqrexlemcalc3  9588  resqrexlemnm  9590  resqrexlemcvg  9591  absneg  9622  abscj  9624  sqabsadd  9627  sqabssub  9628  absmul  9641  absid  9643  absre  9647  absresq  9648  absexpzap  9650  recvalap  9667  abstri  9674  abs2dif2  9677  recan  9679  cau3lem  9684  amgm2  9688  climaddc1  9823  climsubc1  9826  climcvg1nlem  9842  serif0  9845
  Copyright terms: Public domain W3C validator