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

Theorem oveq2d 5556
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 5548 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259  (class class class)co 5540
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rex 2329  df-v 2576  df-un 2950  df-sn 3409  df-pr 3410  df-op 3412  df-uni 3609  df-br 3793  df-iota 4895  df-fv 4938  df-ov 5543
This theorem is referenced by:  csbov1g  5573  caovassg  5687  caovdig  5703  caovdirg  5706  caov32d  5709  caov4d  5713  caov42d  5715  grprinvlem  5723  grprinvd  5724  grpridd  5725  nnaass  6095  nndi  6096  nnmass  6097  nnmsucr  6098  ecovass  6246  ecoviass  6247  ecovdi  6248  ecovidi  6249  addasspig  6486  mulasspig  6488  distrpig  6489  dfplpq2  6510  mulpipq2  6527  addassnqg  6538  prarloclemarch  6574  prarloclemarch2  6575  ltrnqg  6576  enq0sym  6588  addnq0mo  6603  mulnq0mo  6604  addnnnq0  6605  nq0a0  6613  distrnq0  6615  addassnq0  6618  prarloclemlo  6650  prarloclem3  6653  prarloclem5  6656  prarloclemcalc  6658  addnqprl  6685  addnqpru  6686  prmuloclemcalc  6721  mulnqprl  6724  mulnqpru  6725  distrlem4prl  6740  distrlem4pru  6741  1idprl  6746  1idpru  6747  ltexprlemloc  6763  addcanprleml  6770  addcanprlemu  6771  recexprlem1ssu  6790  ltmprr  6798  caucvgprlemcanl  6800  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  cauappcvgprlem1  6815  cauappcvgprlemlim  6817  caucvgprlemnkj  6822  caucvgprlemnbj  6823  caucvgprlemdisj  6830  caucvgprlemloc  6831  caucvgprlemcl  6832  caucvgprlemladdrl  6834  caucvgprlem1  6835  caucvgpr  6838  caucvgprprlemell  6841  caucvgprprlemcbv  6843  caucvgprprlemval  6844  caucvgprprlemnkeqj  6846  caucvgprprlemopl  6853  caucvgprprlemlol  6854  caucvgprprlemloc  6859  caucvgprprlemclphr  6861  caucvgprprlemexb  6863  caucvgprprlemaddq  6864  caucvgprprlem1  6865  addcmpblnr  6882  mulcmpblnrlemg  6883  addsrmo  6886  mulsrmo  6887  addsrpr  6888  mulsrpr  6889  ltsrprg  6890  recexgt0sr  6916  mulgt0sr  6920  caucvgsrlemgt1  6937  caucvgsrlemoffval  6938  caucvgsr  6944  mulcnsr  6969  pitoregt0  6983  recidpirqlemcalc  6991  axmulcom  7003  axmulass  7005  axdistr  7006  ax0id  7010  axcnre  7013  recriota  7022  axcaucvglemcau  7030  axcaucvglemres  7031  mulid1  7082  adddirp1d  7111  mul32  7204  mul31  7205  add32  7233  add4  7235  add42  7236  cnegex  7252  addcan2  7255  addsubass  7284  subsub2  7302  nppcan2  7305  sub32  7308  nnncan  7309  sub4  7319  muladd  7453  subdi  7454  mul2neg  7467  submul2  7468  mulsub  7470  mulsubfacd  7487  add20  7543  recexre  7643  rereim  7651  apreap  7652  ltmul1  7657  cru  7667  apreim  7668  mulreim  7669  apadd1  7673  apneg  7676  mulap0  7709  divrecap  7741  divassap  7743  divsubdirap  7759  divdivdivap  7764  divmul24ap  7767  divmuleqap  7768  divcanap6  7770  divdivap1  7774  divdivap2  7775  divsubdivap  7779  conjmulap  7780  div2negap  7786  apmul1  7839  cju  7989  nnmulcl  8011  add1p1  8231  sub1m1  8232  cnm2m1cnm3  8233  xp1d2m1eqxm1d2  8234  div4p1lem1div2  8235  un0addcl  8272  un0mulcl  8273  zaddcllemneg  8341  qapne  8671  cnref1o  8680  lincmb01cmp  8972  iccf1o  8973  ige3m2fz  9015  fztp  9042  fzsuc2  9043  fseq1m1p1  9059  fzm1  9064  ige2m1fz1  9073  nn0split  9096  fzval3  9162  zpnn0elfzo1  9166  fzosplitsnm1  9167  fzosplitprm1  9192  fzoshftral  9196  rebtwn2zlemstep  9209  flhalf  9252  modqval  9274  modqvalr  9275  modqdiffl  9285  modqfrac  9287  flqmod  9288  intqfrac  9289  zmod10  9290  modqmulnn  9292  modqvalp1  9293  modqid  9299  modqcyc  9309  modqcyc2  9310  modqmul1  9327  q2submod  9335  modqdi  9342  modqsubdir  9343  modqeqmodmin  9344  modsumfzodifsn  9346  addmodlteq  9348  iseqeq3  9380  iseqval  9384  iseqp1  9389  iseqm1  9391  iseqfveq2  9392  iseqshft2  9396  monoord2  9400  isermono  9401  iseqsplit  9402  iseqcaopr3  9404  iseqcaopr2  9405  iseqcaopr  9406  iseqhomo  9412  iseqz  9413  expivallem  9421  expival  9422  expp1  9427  expnegap0  9428  expineg2  9429  expn1ap0  9430  expm1t  9448  1exp  9449  expnegzap  9454  mulexpzap  9460  expadd  9462  expaddzaplem  9463  expaddzap  9464  expmul  9465  expmulzap  9466  m1expeven  9467  expsubap  9468  expp1zap  9469  expm1ap  9470  expdivap  9471  iexpcyc  9523  subsq2  9526  binom2  9529  binom21  9530  binom2sub  9531  mulbinom2  9533  binom3  9534  zesq  9535  bernneq  9537  sqoddm1div8  9569  nn0opthlem1d  9588  nn0opthd  9590  facp1  9598  facnn2  9602  faclbnd  9609  faclbnd6  9612  bcval  9617  bccmpl  9622  bcn0  9623  bcnn  9625  bcnp1n  9627  bcm1k  9628  bcp1n  9629  bcp1nk  9630  ibcval5  9631  bcp1m1  9633  bcpasc  9634  bcn2m1  9637  bcn2p1  9638  shftcan1  9663  shftcan2  9664  cjval  9673  cjth  9674  crre  9685  replim  9687  remim  9688  reim0b  9690  rereb  9691  mulreap  9692  cjreb  9694  recj  9695  reneg  9696  readd  9697  resub  9698  remullem  9699  imcj  9703  imneg  9704  imadd  9705  imsub  9706  cjcj  9711  cjadd  9712  ipcnval  9714  cjmulrcl  9715  cjneg  9718  addcj  9719  cjsub  9720  cnrecnv  9738  caucvgrelemcau  9807  cvg1nlemcau  9811  cvg1nlemres  9812  recvguniqlem  9821  resqrexlemover  9837  resqrexlemlo  9840  resqrexlemcalc1  9841  resqrexlemcalc3  9843  resqrexlemnm  9845  resqrexlemcvg  9846  absneg  9877  abscj  9879  sqabsadd  9882  sqabssub  9883  absmul  9896  absid  9898  absre  9904  absresq  9905  absexpzap  9907  recvalap  9924  abstri  9931  abs2dif2  9934  recan  9936  cau3lem  9941  amgm2  9945  climaddc1  10080  climsubc1  10083  climcvg1nlem  10099  serif0  10102  dvdsexp  10173  oexpneg  10188  opeo  10209  omeo  10210  m1exp1  10213  flodddiv4  10246  flodddiv4t2lthalf  10249  pw2dvdslemn  10253  pw2dvdseulemle  10255  pw2dvdseu  10256  oddpwdclemxy  10257  oddpwdclemdvds  10258  oddpwdclemndvds  10259  oddpwdclemdc  10261  qdencn  10511
  Copyright terms: Public domain W3C validator